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.