Lesson 7.9's formal run catches 7 of the 24 Bug Zoo bugs. The other 17 are not formal's failures in any simple sense: some are deeper than the proof's bound, some break rules nobody wrote as formal properties, and some are about counts accumulated over hundreds of packets. Lesson 6.9's simulation testbench catches all 24. The split is not an accident; it follows the shapes of logic each method handles.
When is formal the wrong tool, and simulation the right one?
The obvious conclusion from lesson 7.5 is to prove everything that can be proved and simulate the rest. In practice the boundary is about cost and reach, not possibility. Formal cost grows steeply with depth and state (lesson 7.2), every property must be written, and a chip runs software for billions of cycles. Simulation's cost grows only linearly with cycles, and its checks can be end-to-end comparisons against models that would be impractical as properties.
Where simulation wins | Why | DCRouter example |
|---|---|---|
Deep state and long sequences | Formal's cost explodes with depth; simulation's grows linearly | BUG_1 (FIFO full) needs at least 10 cycles, BUG_22 at least 13, BUG_15 hundreds |
Wide data transformations | Arithmetic, CRCs and encodings make solvers slow | CRC checking (BUG_12, BUG_13) is natural for a scoreboard with a reference model |
Results accumulated over many transactions | Counts and statistics are easy to compare at the end of a run | PKT_CNT, ERR_CNT (BUG_11, 14, 16, 19) |
Whole systems and software | Formal does not scale to processors running code | DCRouter inside an SoC with a driver (Part 8) |
Rules not written as properties | Formal checks only what is stated | Most register rules had no formal property here |
Performance and statistics | Throughput and latency distributions need long runs | Fairness over time (lesson 5.9) |
Reason | Bugs |
|---|---|
A property covers the rule, but the bug is deeper than the depth-7 bound (lesson 7.9's full proof by induction catches both) | BUG_1 (FIFO full), BUG_22 (credits during sleep) |
No formal property covers the rule (packet framing, error flags, counters, registers, configuration, sleep and wake) | BUG_3, 4, 8, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 23 |
Neither reason is fixed by "more formal" alone. More properties would catch some (a reset-value property would catch BUG_17 in the first cycle after reset), deeper or inductive proofs others, but each costs effort that simulation's existing scoreboard and register checks already spent. The right question is not "can formal do it?" but "what is the cheapest strong evidence for this rule?"
Its states are hundreds of cycles deep and no small configuration reaches them.
It is about data values computed by wide arithmetic.
It involves software, other blocks or the whole chip.
It is statistical: averages, distributions, throughput.
An end-to-end reference model expresses it more simply than properties do.
Practice | Purpose |
|---|---|
Formal for control blocks, simulation for data paths and systems | Each method where its cost is low |
Formal and simulation results merged per rule | One evidence ledger regardless of method (lesson 7.8) |
Re-evaluating the split as tools and designs change | Yesterday's too-deep property may be today's easy proof |
A team (illustrative) mandated formal for every block. The data-path blocks' proofs never converged, engineers wrote weaker and weaker properties to make them finish, and the eventual "proved" results checked almost nothing. A scoreboard against the existing C model would have given strong evidence in a week. Formal everywhere is as much a mistake as formal nowhere.
The CRC is wide data computation over a whole packet; a reference model computes it directly, while a solver must reason about it symbolically over many cycles.
BUG_17: a property that CTRL holds 0x3F after reset fails in the first cycle after reset. BUG_15: saturation after 255 errors is far beyond a short bounded proof.
Simulation wins on deep state, wide data, accumulated results, whole systems, statistics and unwritten rules.
DCRouter's proofs missed 17 bugs: 2 deeper than the bound, 15 outside the property set.
Assign each rule to the cheapest strong evidence, not to a method by policy.