DCRouter's round-robin bug, BUG_5, took this course four lessons to catch in simulation: random traffic reached it constantly, but only a purpose-built arbitration checker could see it (lesson 5.10). The formal proofs of lesson 7.9 found it in step 4, with no stimulus at all, from one property about how the pointer must move.
What kinds of logic are better proved than tested?
The obvious rule is "use formal for small blocks". Size matters, but the better guide is the kind of behaviour. Formal's strength is exhaustive reasoning over a few cycles about a modest amount of control state; its weakness is long sequences and wide data. A small block full of arithmetic can be hopeless for formal, while a large block whose risky part is a small arbiter can be ideal.
Kind of logic or rule | Why formal wins | DCRouter example |
|---|---|---|
Arbiters and schedulers | Every combination of requests in every state, including the rare ones | BUG_6, 7: counterexample in step 3 |
FIFOs, counters and credit loops | Invariants such as count bounds and conservation of credits | BUG_10: step 2; BUG_9: step 6 |
Handshakes and protocols | Every timing of valid, ready and stalls | R1 and R13 rules as assertions |
Coincidences of a few signals | Simultaneous events that random stimulus rarely aligns | BUG_2 (push and pop together): step 5 |
"Never" and "always" rules | A proof covers all executions; simulation samples a few | No credit is ever lost or invented |
Deadlock and liveness | Can reason about whether progress is always possible | A locked output is always eventually released (with the right tools) |
Routing and decoding | Every address or header value at once | BUG_24 (stale destination): step 6 |
Bug | First simulation catch in this course | Formal (lesson 7.9) |
|---|---|---|
BUG_5 | Lesson 5.10: purpose-built arbitration checker | Step 4 |
BUG_6, BUG_7 | Lesson 5.10, only with the hot-spot phases | Step 3 |
BUG_9 | Lesson 4.1's credit check and later audits | Step 6 |
BUG_24 | Lesson 4.7: varied back-to-back traffic | Step 6 |
For the bugs within reach of its bound, formal needed no stimulus design, no checker timing model and no seeds: one property per rule and a solver.
Few cycles to the interesting states: a 4-deep FIFO, not a 1,024-deep one (or use a small configuration).
Rules about relations, not computed values: "granted means requesting", not "the FFT is right".
Rare coincidences matter: several conditions in one cycle.
High cost of escape: arbitration, coherence, security and safety logic where "never" must really mean never.
Practice | Purpose |
|---|---|
Formal plans per block, listing properties and target proof depth | Formal effort aimed where it wins |
Designer-run formal on new control logic | Bugs found before simulation environments exist |
Formal sign-off for critical control blocks | Proofs instead of coverage for the highest-risk logic (Part 14) |
A team (illustrative) proved its interconnect arbiter exhaustively and left the address decoder to simulation, since "decoders are simple". A two-region overlap in the decode map, reachable only by one address range, escaped to silicon. Decoders are a formal sweet spot: every address at once is exactly what a solver does well.
The property states how the round-robin pointer must move after every grant; the solver finds the first grant where it does not, while simulation needed a purpose-built fairness checker to turn the stuck pointer into a visible failure.
Good: credits are conserved (R7); the arbiter grants the specified winner (R6). Poor: a 255-error counter saturates (R9) needs hundreds of cycles; payload data integrity through long packets is better checked by the scoreboard.
Formal wins on control: arbiters, FIFOs, counters, handshakes, decoders, deadlock.
It finds rare coincidences without stimulus design, and proves "never" within its reach.
Choose targets by the shape of the risk, not only by block size.