Assertion-based verification (ABV) is a methodology in which designers use assertions to capture specific design intent and, either through simulation, formal verification, or emulation of these assertions, verify that the design correctly implements that intent.
A simple example would be a design that contains a block that should implement a FIFO. Using an ABV methodology the designer would define assertions that capture the design intent (in this case, that neither overflow nor underflow of the IFO may occur) and through simulation, formal verification, or emulation verify that the FIFO is correctly implemented.
With language and tool support for assertions widely available, designers and verification engineers have embraced ABV methodologies to improve design quality and verification productivity. Moreover, designers have found assertions to be invaluable in the debugging process.
A comprehensive ABV flow leverages assertion libraries and user-defined assertions that are used in simulation, formal verification, and emulation or FPGA-based prototyping while collecting coverage information in a coverage database like Questa’s Unified Coverage DataBase (UCDB).
The ABV methodology is easy to adopt in most existing verification flows since it can be adopted incrementally. Specifically, using assertion libraries is a great way to introduce ABV in any project. The rich assertion libraries that accompany the Questa and Questa Formal Verification products allow you to add high-value assertions to your design and immediately get the benefits, yielding a high ROI even on the first project.
- Assertions actively monitor a design (or testbench) to ensure correct functional behavior
- Assertions detect design errors at their source, greatly increasing observability and decreasing debug time
- With assertion languages like SVA (part of SystemVerilog) and PSL standardized, the ABV methodology today is supported by a wide array of tools and work with Verilog, SystemVerilog, and VHDL designs
- The availability of assertion libraries, for example Mentor’s Questa and Questa Formal Verification product both include a rich assertion library, ABV is easy to adopt
- Assertions have a high ROI in that they can be used across simulation, formal verification, and even emulation
Mentor’s support for ABV
Mentor’s functional verification solution has broad and deep support for ABV. Not only do the core verification tools like Questa, Questa Formal Verification, and Veloce support all standard assertion libraries and languages, they also provide dedicated support, for example, in debugging and coverage directly related to assertions.