This course assumes a foundational understanding of digital design principles and hardware description languages (HDLs), with familiarity with PSL being beneficial but not mandatory. Prior experience in formal verification is advantageous but not required. A background in IC design or verification is preferred. Proficiency in basic programming and digital logic is necessary, along with access to formal verification tools for executing PSL assertions.

ABV is a form of whitebox testing. That is, properties—asserted behaviors—can monitor behavior deep within the design and not just at the interfaces. This feature lets you identify errors sooner and closer to the source, and also lets you specify functional coverage points deep within the design. The following are the primary technologies that use assertions: First, Simulation, Dynamic checking of monitors in simulation. Second, Formal Analysis, Static property checking tools are used to prove that a property that is asserted will hold true for all input conditions that do not violate an assumed behavior. Third, Emulation/Acceleration, Another form of dynamic ABV that uses a emulation accelerator. Some verification goals are well-suited for ABV technologies, and other goals might be handled better by other tools. The key is to use ABV where you get the best return on investment.

ABV technologies can isolate functional errors close to their source. The advantages of using ABV in different areas is explained below: First, Using ABV for Error Detection. Simulation Stimulus Errors, Protocol Errors, Design Errors, Performance Requirements, Hard-to-Find Corner Cases, Errors Caused by State Machine Interactions. Second, Using Assertions as Coverage Points. Coverage points that are expressed using assertion languages can help ensure that the device is well tested. These coverage points: Identify holes in the tests Eliminate inefficient or redundant tests. Third, Using Assertions for Transaction Viewing. Transactions recorded from an assertion simulation are displayed in the waveform debug tool in the same way as other transactions. You can graphically view assertion failures in the context of the other activity in your system.

Assertion-based verification (ABV) means different things to different people. The application of assertion technologies and the languages associated with them have continued to evolve over time. As assertion languages are designed to express complex behavior, technologies evolve to make use of them.

Leverage assertions and translate design specifications into assertions. Assertions are written by various people at various times during the development of a product, from conception through design and implementation, and during verification. Assertions can be written at different levels of abstraction, in various hardware design language contexts. Assertions take some effort to write. At the same time, they can make design verification much more efficient, can simplify debugging, and can significantly improve overall productivity.

PSL is a language which is IEEE standard 1850, and it has a strong history of development. It is a powerful property specification language that can describe complex behaviors in very few characters. PSL has the power to define complex properties which, although useful for formal verification, cannot be easily evaluated in simulation. The PSL Language Reference Manual defines a simple subset for the language which is easily simulated.

PSL describes the behavior of a design from a verification perspective, using properties to describe what the design should and should not do. The course provides many practical methods for using PSL language, as well as recommended coding styles, common PSL issues and how to avoid them, and the pros and cons of different methods of placing PSL.

Assertion-based verification (ABV) is a verification approach where the user specifies design properties in SVA/PSL language and considers assertions as a primary means of verification at each verification stage, while also combining various verification techniques and gradually adopting ABV in the verification flow. This course explores the different verification stages and the verification breakthroughs driven by assertion verification techniques.

The ABV methodology can be applied to formal, simulation, and acceleration verification. Each verification technique corresponds to different verification tools. Based on the advantages and disadvantages of each verification technique, use assertions reasonably and effectively. Many verification environment indicators can be collected in the verification flow. The assertion results reported in formal, simulation, and acceleration verification can be collected together to maximize the achievement of verification metrics.

ABV technologies can isolate functional errors close to their source. The advantages of using ABV in different areas is explained below: First, Using ABV for Error Detection. Simulation Stimulus Errors, Protocol Errors, Design Errors, Performance Requirements, Hard-to-Find Corner Cases, Errors Caused by State Machine Interactions. Second, Using Assertions as Coverage Points. Coverage points that are expressed using assertion languages can help ensure that the device is well tested. These coverage points: Identify holes in the tests Eliminate inefficient or redundant tests. Third, Using Assertions for Transaction Viewing. Transactions recorded from an assertion simulation are displayed in the waveform debug tool in the same way as other transactions. You can graphically view assertion failures in the context of the other activity in your system.