Simulation and formal, side by side
Formal does not replace simulation. The two answer different questions, and mature teams plan which one owns which part of the verification job. The table below compares them on the points that matter most in practice.
| Simulation | Formal property verification | |
|---|---|---|
| You write… | Stimulus (tests, sequences) and checkers | Assertions, assumptions and covers |
| Inputs explored | Only the ones your tests generate | All legal input sequences |
| Result for a check | Passed in the tests run | Proven / failed with CEX / bounded to N cycles |
| Failure trace length | Often thousands of cycles | Usually the shortest possible path |
| Design size | Whole chip, with emulation for speed | Best on blocks; full chip only for special apps |
| Good at | Long scenarios, software interaction, performance | Corner cases, control logic, concurrency, protocols |
| Weak at | Rare corner cases, proving absence of bugs | Very deep sequential behaviour, wide datapaths like multipliers |
A mental model: depth versus breadth
Think of all behaviours of a design as a tree that starts at reset and branches on every cycle. Simulation follows a few very long branches deep into the tree. Formal looks at every branch, but the effort grows with how far from reset it must look. That is why formal shines on logic where interesting behaviour happens within tens of cycles — arbiters, FIFOs, FSMs, handshakes, schedulers — and why deep datapath pipelines often need help.
When should a block get formal?
A quick rule of thumb used by many teams: a block is a good formal candidate when it is control-heavy (lots of decisions, concurrency and corner cases), has clear interface rules you can write as assumptions, and its interesting behaviour happens within a modest number of cycles of reset or of a transaction start. Arbiters, credit/flow control, cache controllers, interrupt logic, power-management sequencers, and bus bridges are classic examples.