Formal Property Verification
Formal Property Verification is the mathematical technique that exhaustively proves or disproves whether a design satisfies a specified property for ALL possible input sequences — providing complete verification coverage that simulation can never achieve, detecting corner-case bugs that would require billions of simulation cycles to encounter, and serving as a critical signoff methodology for safety-critical and high-reliability chip designs.
Formal vs. Simulation
| Aspect | Simulation | Formal Verification |
|---|---|---|
| Coverage | Samples (10⁶-10⁹ vectors) | Exhaustive (ALL possible inputs) |
| Bug finding | Finds common bugs | Finds corner-case bugs |
| Proof capability | Cannot prove absence of bugs | Can PROVE property holds |
| Scalability | Any design size | Limited (< 100K-500K gates effectively) |
| Setup effort | Testbench + stimuli | Properties + constraints |
Formal Techniques
| Technique | Application | Tool |
|---|---|---|
| Equivalence Checking (LEC) | RTL vs. netlist, pre/post-ECO | Conformal (Cadence), Formality (Synopsys) |
| Model Checking | Property verification (SVA assertions) | JasperGold (Cadence), VC Formal (Synopsys) |
| Sequential Equivalence | Verify retiming, sequential optimization | Same tools with sequential mode |
| X-propagation | Verify correct X handling in resets | Formal X-prop analysis |
| Connectivity | Verify signal connectivity in SoC | Formal connectivity checking |
Equivalence Checking (Most Widely Used)
- Compares two designs: Reference (RTL) vs. Implementation (gate-level netlist).
- Proves every output is functionally identical for all inputs.
- Used after: Synthesis, P&R, ECO — each step verified against golden RTL.
- Runs in minutes-hours for even billion-gate designs.
Model Checking (Property Verification)
- User writes properties in SVA: "Request always followed by acknowledge within 5 cycles."
- Formal tool explores ALL reachable states of the design.
- If property violated → tool provides counterexample (specific input sequence that breaks property).
- If property holds → mathematical proof (bounded or unbounded).
Bounded vs. Unbounded Proof
- Bounded Model Checking (BMC): Prove property for first N cycles (N = 10-100).
- Fast, finds bugs quickly, but not a complete proof.
- Unbounded (Full Proof): Prove property for ALL time — requires finding inductive invariant.
- Harder, may timeout on complex designs — but provides absolute guarantee.
Formal Verification in Design Flow
1. RTL phase: Model checking on blocks (< 100K gates) — prove protocol, FSM, datapath properties.
2. Post-synthesis: LEC (RTL vs. gate netlist).
3. Post-P&R: LEC (synthesis netlist vs. P&R netlist).
4. Post-ECO: LEC (original vs. ECO'd netlist).
5. Signoff: All LEC clean, all critical properties proven.
Formal property verification is the mathematical foundation of chip design correctness — while simulation tests what you think of, formal verification proves properties hold for scenarios you never imagined, making it indispensable for catching the subtle corner-case bugs that would otherwise escape to silicon.