Simulation samples behaviors. Formal explores the state space under given assumptions.
Question | Simulation | Formal |
|---|---|---|
Coverage | Samples chosen behaviors | Explores every behavior under the assumptions |
Result on a pass | The sampled runs pass | The property holds inside the bound |
Needs | Stimulus and checkers | Properties and environment assumptions |
Misses | Corners no seed visits | Anything outside the assumptions or the bound |
4 lessons, about 23 min
Any behavior after cycle 20 that the random runs did not happen to sample, and anything the formal assumptions exclude. Inside the bound, BMC covers every input sequence; beyond it, only the sampled runs speak.
The whole topic on one page, taken from each lesson's Remember box. Read it before an interview, or print it.
What formal adds beyond simulation
Each simulation seed walks one path; formal explores the state space under given assumptions.
A pass at depth N is bounded assurance; an unbounded proof needs a complete method.
Formal wins on control corners and protocol invariants. Simulation stays essential for datapaths and long sequences.
Rule of thumb: read the actual task result; PASS, FAIL, UNKNOWN and ERROR are not interchangeable.
Assumption discipline
Every strong assumption should map to an interface or protocol guarantee, and be reviewed like an assertion.
If the trigger never fires, the implication holds with no check on the grant logic.
Zero cover hits in simulation mean non-exercise; a bounded formal miss means no witness within that depth.
Rule of thumb: weaken assumptions until legal stress passes through.
When formal helps most
Formal pays back fastest on small control logic with a large state space: FIFOs and arbiters.
Pair each obligation with an exact-trigger cover; a bounded cover miss is inconclusive beyond its depth.
Eventual service gives eventual progress. A numeric deadline needs a maximum service gap and persistent request ownership.
Rule of thumb: state the service-gap and persistence assumptions before you derive the bound.
Your First Formal Run
A bounded pass covers its depth from reset. Induction covers every cycle, but it starts from any state that satisfies the assertions, reachable or not.
When induction fails, check step 0 of its trace: an unreachable start state needs a helper assertion, proved like any other.
An over-constrained assume makes a buggy design pass. Cover the inputs your asserts depend on.
Rule of thumb: a formal pass means nothing until you know its depth, its assumptions and whether induction closed.
Mini project: a reusable FIFO IP with package, interface, assertions and a formal check
Practice question: FSM formal verification of liveness and safety
Code lab: Formal vacuity check
Practice question: Formal-friendly CDC FIFO checkers
Code lab: Synchronous FIFO (4 entries)
Interview: run a mock interview on this topic
All simulation benches here are finite exercises, not formal proofs. Executed with Icarus Verilog 13.0 (2026-10-16): each prints PASS. Each bench declares 1ns/1ps time units and terminates unexpected failures with a diagnostic $fatal(1, ...); $finish follows PASS. The repository runner recognizes FAIL markers in logs, whereas copied standalone automation also needs failing process termination.