Where formal fits in a chip project
"Using formal" can mean several quite different activities. It helps to name them, because each has different goals, effort and exit criteria.
The main usage models
| Usage model | Goal | Typical effort | Covered in |
|---|---|---|---|
| Design exploration | Help the designer understand and sanity-check fresh RTL using covers and a few assertions | Hours to days | Chapter 5 |
| Bug hunting | Find corner-case bugs in a block that simulation also verifies | Days to weeks | Chapter 6 |
| Signoff (full proof) | Formal is the primary verification of the block; proofs replace simulation tests | Weeks | Chapters 6, 11 |
| Formal apps | Push-button flows for specific problems: connectivity, registers, X-propagation, unreachable coverage | Hours to days | Chapter 7 |
| Equivalence checking (FEV) | Prove two models (e.g. RTL and netlist) behave identically | Mostly automated | Chapter 8 |
| Post-silicon debug | Reproduce a failure seen in the lab by searching for a trace that matches the symptoms | Days | Chapter 7 |
Formal equivalence checking between RTL and gate-level netlists is so mature that almost every chip uses it, often without the RTL team thinking of it as "formal". Property verification and formal apps are where most of the learning curve — and most of the value — lies, and they are the focus of this course.