formal verification basics

**Formal Verification** — using mathematical proofs to verify hardware correctness exhaustively, without simulation test vectors. **Types** - **Equivalence Checking (EC)**: Prove two designs are functionally identical - RTL vs. RTL (after modification) - RTL vs. gate netlist (after synthesis) - Gate netlist vs. gate netlist (after ECOs) - Tools: Synopsys Formality, Cadence Conformal - **Model Checking / Property Checking**: Prove specific properties hold for all possible inputs - "The FIFO never overflows" - "The arbiter never grants two masters simultaneously" - "No deadlock in the protocol" - Written as SVA (SystemVerilog Assertions) - Tools: Cadence JasperGold, Synopsys VC Formal **Advantages Over Simulation** - Exhaustive: Covers ALL possible input sequences (simulation covers only tested ones) - Finds corner cases humans miss - Can prove absence of bugs (not just presence) **Limitations** - State space explosion: Cannot handle full chip — works on blocks - Requires expertise to write meaningful properties - Some properties are undecidable **Formal verification** is now mandatory for safety-critical designs (automotive, aerospace) and widely used for protocol verification and post-synthesis checking.