Assertion Based Verification
Assertion-Based Verification (ABV) is the methodology of embedding formal property specifications directly into RTL code to continuously monitor design correctness during simulation and formal analysis — catching bugs at the point of occurrence rather than relying on downstream output checking, reducing debug time from days to minutes for complex SoC designs.
What Are Assertions?
- Assertions: Formal statements that declare "this property must always be true."
- Example: `assert property (@(posedge clk) req |=> ##[1:3] ack);` — After request, acknowledge must come within 1-3 cycles.
- Violation: If the property fails during simulation, the simulator flags the exact cycle and signal state — no need to trace backwards from output.
SystemVerilog Assertion (SVA) Types
| Type | Syntax | Purpose |
|---|---|---|
| Immediate | `assert (a == b)` | Checks at current time — like an if-statement |
| Concurrent | `assert property (...)` | Checks across multiple clock cycles — temporal |
| Assume | `assume property (...)` | Constrains inputs (for formal — tells solver what inputs are legal) |
| Cover | `cover property (...)` | Tracks whether a scenario occurred — coverage analysis |
| Restrict | `restrict property (...)` | Limits formal search space |
SVA Temporal Operators
- `|->`: Overlapping implication (same cycle).
- `|=>`: Non-overlapping implication (next cycle).
- `##N`: Delay by N cycles.
- `##[M:N]`: Delay by M to N cycles (range).
- `$rose(sig)`: Signal transitioned 0→1.
- `$fell(sig)`: Signal transitioned 1→0.
- `throughout`: Condition holds for entire sequence.
ABV Methodology
- White-Box Assertions: Written by the designer, embedded inside the RTL module — checks internal invariants.
- Black-Box Assertions: Written by the verification team, bound to module ports — checks interface protocol.
- Protocol Monitors: Reusable assertion libraries for standard protocols (AXI, AHB, PCIe).
- Coverage Integration: Assertion coverage tracks how many properties were exercised.
Formal Verification with SVA
- SVA properties can be proven exhaustively using formal tools (JasperGold, VC Formal).
- Formal proves the property holds for all possible input sequences — not just simulation vectors.
- Limitations: State space explosion for large designs — formal works best on block-level (< 100K gates).
Assertion-based verification is the standard methodology for complex SoC verification — embedding executable specifications directly in RTL catches bugs at the source, enables formal exhaustive proofs, and provides measurable coverage metrics that are required for tapeout signoff.