Simulation samples behaviors. Each seed walks one path through the state space.
Random seeds cover surprising paths, and handcrafted tests pin known corners. Control logic still hides interleavings that no seed visits.
Formal explores the state space under given assumptions. Bounded model checking tests each property up to a bounded depth and returns a counterexample on failure.
The search aims at the property directly. Short counterexamples appear without handcrafted stimulus.
The two methods complement each other. Simulation stays essential for datapaths and long sequences. Formal wins on corner-case control logic and protocol invariants.
A pass at depth N says nothing about cycle N+1. Treat it as bounded assurance, never as an unbounded proof.
Claim | What it means | What is still open |
|---|---|---|
Bounded pass to depth 20 | No failure in the first 20 cycles under the assumptions | Cycle 21 and beyond |
Full proof | No failure at any depth, usually by induction | Only as strong as the assumptions |
Simulation pass | The sampled runs pass | Every unsampled run |
The repository includes scripts/examples/rtl-formal/grant.sv, grant.sby and a README. The harness uses immediate formal assertions supported by the Yosys frontend rather than requiring its parser to accept full temporal SVA. With Yosys, SymbiYosys and the Z3 solver already installed, run the three tasks below from the repository checkout.
cd scripts/examples/rtl-formal
sby -f grant.sby bmc
sby -f grant.sby prove
sby -f grant.sby cover// snippet: excerpt from grant.sv, inside its clocked formal harness
// Reset is asserted at the first sampling edge; later requests are unconstrained.
// History is used only after three post-reset samples exist.
if (history == 3) begin
assert(gnt == $past(req, 3));
cover(gnt && $past(req, 3));
endThe property uses pre-update clock-edge samples: three register stages mean gnt equals req from three sampled edges earlier. This differs from the post-update cycle labels in the simulation below. The BMC task checks to depth 12; the prove task attempts an unbounded inductive proof; cover searches for a reachable request/grant witness. Read the actual task result: PASS, FAIL, UNKNOWN or ERROR are not interchangeable. An unreachable cover is a reachability result, not a proof of the response obligation.
The trace below is simulation evidence for one request. A grant answers two cycles after its request, matching the exact-latency property; there is no window, so a grant at any other latency fails. Inputs change half a cycle before the edge that starts their slot, so the edge at the start of slot 2 captures req, and gnt updates two edges later, at the start of slot 4.
Slot 1: reset holds, req 0, gnt 0.
Slot 2: req rises, gnt still 0.
Slot 3: req held, gnt still 0.
Slot 4: req drops, gnt answers.
Slot 5: gnt holds one more cycle.
Slot 6: the pipeline drains, gnt 0.
No. Sampling never covers every interleaving. A bounded liveness check covers every interleaving inside its window instead.
Nothing. The guarantee ends at the bound. A separate cover search can find an interesting-state witness; a bounded miss does not establish unreachability or erase the bounded property result.
Exhaustive search aims at the property directly instead of hoping a seed stumbles onto the corner.
Do | Avoid |
|---|---|
Read a bounded pass as assurance inside the bound | Calling it a proof at every depth |
Pair every property with cover on its antecedent | Trusting a pass whose trigger never fired |
Keep simulation for datapaths and long runs | Dropping simulation once formal passes |
The grant pipeline plus a testbench that checks 2000 LFSR cycles against a two-cycle reference.
module grant_delay (
input logic clk, rst_n, req,
output logic gnt
);
logic r1, r2;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin r1 <= 1'b0; r2 <= 1'b0; gnt <= 1'b0; end
else begin r1 <= req; r2 <= r1; gnt <= r2; end
end
endmodule
Testbench run with Icarus Verilog 13.0 (2026-10-16): prints PASS. It checks 2000 LFSR cycles against a two-cycle reference. The repository exercise (grant.sv, grant.sby) is given as instructions to run; no proof run is reported for this lesson. All benches here are finite exercises, not formal proofs.