Assertion Based Verification (ABV) is a technique in which assertions are used as the primary means of verifying the correctness of a digital design. Assertions are statements that describe a condition that must always be true within a design, and are typically written in a hardware description language such as SystemVerilog or VHDL.
The basic idea behind ABV is to use a combination of functional and formal verification techniques to verify that the design meets its functional requirements. SystemVerilog Assertions are used to define the expected behavior of the design, and formal verification techniques are used to check that the design satisfies these assertions under all possible conditions.
ABV can be used at various stages of the design process, including design validation, module-level verification, and full-chip verification. By using assertions as the primary means of verifying a design, ABV can help to reduce the amount of time and effort required for verification, while improving the quality and reliability of the design.
Example
An example of assertion-based verification could be verifying the correctness of a FIFO design.
Assume that we have a FIFO with a width of 8 bits and a depth of 16. The design has read and write pointers to keep track of the data. To verify the design, we can use assertion-based verification by writing assertions to check the following:
- The write pointer should never wrap around and overwrite valid data.
- The read pointer should never wrap around and read stale data.
- The number of elements in the FIFO should never exceed the depth of the FIFO.
- When the FIFO is full, the write operation should not be allowed.
- When the FIFO is empty, the read operation should not be allowed.
These assertions can be written in SystemVerilog Assertions (SVA) syntax and used to verify the design automatically during simulation. By using assertion-based verification, we can verify the design more comprehensively and efficiently than traditional simulation-based verification.
assert property ( @(posedge clk) disable iff (!rst_n)
(in_fifo_wr && !in_fifo_full) ##[1:$] !in_fifo_empty && !in_fifo_wr );
This assertion checks that when the write enable signal in_fifo_wr is high and the FIFO is not full !in_fifo_full , then there should be at least one cycle where the FIFO is not empty !in_fifo_empty and the write enable signal is low !in_fifo_wr . The disable iff !rst_n condition ensures that the assertion is disabled during reset.
Limitations
Some limitations of assertion-based verification include:
- Limited scope: Assertions only check specific aspects of the design and may not provide a complete picture of the design's behavior.
- Time-consuming: Writing assertions can be a time-consuming process, particularly for complex designs. It requires significant effort to write and debug complex assertions.
- False negatives and false positives: Assertions can produce false positives (assertions that fail even though the design is correct) or false negatives (assertions that pass even though the design is incorrect). These issues can be difficult to diagnose and correct.
- Incomplete coverage: Assertions may not cover all possible design scenarios and corner cases.
- Limited debugging: Debugging failures in assertions can be difficult since the assertions are typically executed automatically and do not provide detailed information on what went wrong.
- Limited support for legacy designs: Legacy designs may not have been designed with assertion-based verification in mind and may not have the necessary instrumentation to support it.
