Part 4's random hunt sent a few hundred packets per seed and caught BUG_21 with 16 seeds out of 20. Four seeds never produced the situation that triggers it. That is the nature of simulation: each run is one path through an enormous space, and a bug is found only if some run walks through it. Formal verification asks a different question: is there any path, of any input sequence the environment allows, that breaks this property?
How does formal verification differ from simulation, and what does it give you?
The obvious picture is that formal is simulation with every input tried, which sounds impossible: DCRouter has about 120 input bits per cycle (lesson 0.4 counts 119), so even 10 cycles have about 2^1190 input sequences. Formal tools do not enumerate them. They translate the design and a property into logic and ask a solver whether any assignment of inputs over the cycles makes the property false. The solver reasons about all sequences symbolically, and either proves there is none or produces one.
Simulation | Formal | |
|---|---|---|
Inputs | One sequence per run, chosen by stimulus | Every sequence the assumptions allow |
Result | This run passed or failed | Proof, counterexample, or inconclusive within a bound |
Needs | Stimulus, checks, a reference | Properties and assumptions |
Finds rare corners | Only if a run reaches them | Yes, if they are within reach of the proof |
Scales to | Whole chips and software | Blocks and control logic; cost grows quickly with depth and state |
Shows absence of bugs | Never | For the stated property, under the stated assumptions |
Properties: the rules, written as assertions (lesson 5.3); formal checks nothing you do not state.
Assumptions: what the environment may do; too few give false counterexamples, too many hide bugs (lesson 7.4).
A bound or an argument: either a depth for a bounded check (lesson 7.2) or invariants for a full proof (lesson 7.3).
A design small enough: cost grows with state and depth, so formal targets blocks, not whole chips (lesson 7.6).
When a property fails, the tool returns a trace: the shortest sequence of inputs it found that breaks the property, as a waveform. It is often the clearest bug report a verification engineer ever gets: a handful of cycles, every input chosen to reach the failure, nothing irrelevant. Lesson 7.2's first counterexample is four pushes into a FIFO whose full flag rises too late.
Practice | Purpose |
|---|---|
Formal property verification on control-heavy blocks | Arbiters, FIFOs, counters and protocol logic proved or debugged early |
Assertions shared between simulation and formal | Each property written once, used by both (Part 5) |
Formal applications for specific questions | Equivalence, connectivity, X-propagation (lesson 7.7) |
A team (illustrative) proved every property of an arbiter and declared it verified. The proofs were correct; the arbiter's property set did not include fairness, only mutual exclusion of grants. A starvation bug passed every proof. Formal answers exactly the questions asked: the same lesson as coverage (lesson 6.1), in a different form.
It reasons about all sequences symbolically: the solver searches for any assignment that violates the property, rather than enumerating assignments.
That the properties state the rules that matter (fairness, not just exclusion), and that the assumptions do not exclude legal behaviour (lesson 7.4).
Formal checks a property against every input sequence the assumptions allow.
It returns a proof or a minimal counterexample, never just "this run passed".
It checks only stated properties, under stated assumptions, on designs small enough to reason about.