Choosing where formal signs off
On a real project, formal competes with simulation for engineers and schedule. Picking the wrong block — a huge datapath with vague specs — creates a long, frustrating effort. A quick scoring exercise at planning time helps.
| Criterion | Score 0 | Score 2 |
|---|---|---|
| Control vs datapath | Mostly arithmetic / wide datapath | Mostly decisions, concurrency, protocols |
| Specification quality | Informal, changing | Clear interface rules and behaviour |
| Interface complexity | Many complex, poorly specified interfaces | Few interfaces with standard protocols |
| Sequential depth | Interesting behaviour after thousands of cycles | Within tens of cycles (or abstractable counters) |
| Size of cones | Hundreds of thousands of flops per property | Thousands or fewer |
| Bug risk / history | Stable, reused, well-tested | New, complex, or historically buggy |
Blocks scoring 9–12 are strong signoff candidates; 5–8 suit bug hunting; below 5, use formal apps and leave the rest to simulation. The scores are a conversation starter, not a formula — but they make the trade-offs explicit.
Staffing and schedule
- Start formal when the RTL starts: design exploration (Chapter 5) costs little and pays off immediately.
- Plan signoff effort in weeks per block, including reviews and regression setup.
- Pair a formal engineer with each block's designer; the designer answers spec questions and reviews assumptions.