Assertion-Based Verification

Assertion-Based Verification (ABV) in ASIC design is a verification method in which formal statements (assertions) are used directly in or alongside the design to define and automatically verify correct behavior. Key aspects are:

• Definition of Assertions: Formulation of conditions that must always be true (or true under certain circumstances) – e.g., with SystemVerilog Assertions (SVA).
• Formal verification and simulation: Assertions can be used in both formal tools (static analysis) and simulations to check design rules and detect errors early.
• Documentation and specification alignment: Assertions/Assumptions also serve as a living specification in the code, thus improving comprehensibility and maintainability.
• Debugging aid: During the test run, failed assertions immediately show where and why the design violates specified rules.

Examples:

assert property (@(posedge clk) req |-> ##[1:3] grant);

This assertion requires that a grant be issued 1 to 3 clocks after a req signal.

Conclusion: ABV increases verification quality, saves time during debugging, and supports the formal validation of the design.