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.