Simulation Covers Paths, Formal Covers States

Run the same arbiter through a million random cycles and through a bounded model check, and see why only one of them finds the double grant.

Lesson: F1.1
Time: 15 min
Runs on: SymbiYosys
Check: 4 questions

A three-way arbiter shipped after a million random cycles with assertions on: every grant one-hot, every coverage bin hit. In the field, firmware wrote a new weight register in the same cycle as a burst of requests, and two masters drove the bus together. The bug needed three specific input values in three consecutive cycles. The million cycles were a thin line through a space the bench had never mapped.

The counterexample SBY wrote for the arbiter

Measured with smtbmc yices at depth 20. Three chosen input values in three consecutive cycles, straight after reset.

One Path Through the State Space

Rings of reachable states around reset

Ring k holds every state the arbiter can reach k cycles after reset, under every input sequence. The double grant sits in ring 4. A random run is one thread through these rings.

Four rings hold the double grant 011; a run to depth 20 covers twenty of them. The state 111 (three grants) is outside every ring: no input sequence produces it, so a cover on it would come back unreached.

Read the states and transitions

gnt 000: initial, depth 0.
gnt 010: reachable, depth 1.
lock, 010: reachable, depth 2.
reload 2: reachable, depth 3.
gnt 011: bad, depth 4.
gnt 111: unreachable, depth 0.
gnt 000 → gnt 010.
gnt 010 → lock, 010.
lock, 010 → reload 2.
reload 2 → gnt 011.
gnt 010 → gnt 000.
lock, 010 → gnt 010.

Illustration. A drawing of the idea, with the measured depth. The real arbiter has six flops and 64 possible states; only the ones on the counterexample are drawn.

A simulation is one path through the states of the design: one sequence of inputs, one sequence of states. A million cycles visit at most a million states, out of 2^(flops) possible ones. Coverage says where the path went. It cannot say where the path did not go.

Random run (Verilator)	Measured
Seed	2545F491
Cycles	1,000,000
Weight reloads (one every 4,096 cycles)	244, A5 loaded 0 times
Cycles with two grants	0
Wall time on this machine	578 ms

The bench reloads the weight as firmware would, every 4,096 cycles. Per cycle the chance of the pattern is 1/4096 × 1/256 × 1/8 × 1/8 × 1/8, about 2 in 10^9. A million cycles expect 0.002 hits.

The seed decides the path. A longer run raises the odds and never reaches certainty. The bug in this arbiter needs weight = A5 with req = 110, then req = 011, then req = 111. No bin counts that.

Every State Within k Cycles

The bound and the failure

The task uses depth 20, so this flow checks clocked samples 0 to 18. The buggy arbiter fails at reported step 5 (sampled state 4), well inside the bound.

Linear scale. 0 to 25 steps.

Checked bound: 20
Required bound: 20
First reported failure: 5
Claim: Counterexample found

Required bound here means the task target. The fixed arbiter passes BMC at depth 20 (samples 0 to 18); no unbounded proof is claimed on this page.

A formal tool starts from the reset state and asks, for every possible input at once, which states can be reached in one step, then two, then k. Ring k holds every state k cycles from reset. A property that holds in every ring up to k has been checked against every input sequence of length k, not one of them.

Bounded model checking (BMC) does not pick inputs. It hands the solver one question: is there any input sequence of length k that ends in a bad state? For the double grant the answer is yes at sampled step 4, and the solver returns the inputs as its witness. That is the trace at the top of the page: A5 and 110, then 011, then 111.

Run	Result	Time on this machine
Random bench, 10^6 cycles	Cycles with two grants: 0	578 ms
`sby`, mode `bmc`, depth 20, buggy arbiter	FAIL at reported step 5	652 ms
`sby`, mode `bmc`, depth 20, fixed arbiter	BMC PASS to depth 20	626 ms

Both tools ran the same RTL. The switch between the twins is the tool, not the design.

What Formal Cannot Do

Where Formal Sits Beside SimulationFour ways to check a design. Arrows mean "hands a question to". This lesson runs the first two rows on the same arbiter.

Read the diagram as text

Random simulation: paths; any design size; finds what the stimulus hits
Formal property verification: states; bounded size; finds whatever is reachable
Formal apps: narrow questions on large designs (F5)
Equivalence checking: two designs, same outputs (F6)
arb3 RTL: the same source for every tool

arb3 RTL → Random simulation: one driven path
arb3 RTL → Formal property verification: every input sequence
Formal property verification → Formal apps: the same engines
Formal property verification → Equivalence checking: the same solvers

Formal sits beside UVM, not instead of it. F7.3 says when it can replace a block-level bench.

Formal checks the property you wrote, not the one you meant: a gap in the spec stays a gap. It runs out of room on large designs, because the rings grow with the flop count (F4 is about making proofs finish). It says nothing about analog, timing or anything outside the RTL. It also finds the input values for you: the solver returns them as the model of a satisfiable query (F2.2), so nobody has to guess the firmware's write pattern. The property itself is ordinary SVA (A1.1 Why assertions); the page shows it next to the form this engine runs.

Asked in Interviews

Question	Answer
What does formal prove that a million random cycles cannot?	Every input sequence up to the bound, so every reachable state within it. The random run is one sequence.
When would you not use formal?	Large datapaths without abstraction, properties you cannot state, anything outside the RTL.
How does formal find the input values?	It does not pick them. The solver returns them as the model of a satisfiable query (F2.2).

Try It

Concurrent SVA (what a JasperGold or VC Formal user writes)

assert property (@(posedge clk) disable iff (rst) $onehot0(gnt));

At most one grant bit, every clock, outside reset.

Clocked immediate assertion (what this engine runs)

always @(posedge clk) if (!rst)
  assert($onehot0(gnt));

The same check as a procedural statement. F3.1 teaches the translation.

The whole task. The page leaves depth at the default, 20.

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top arb3
[files]
design.sv

Read the random result
The Verilator bench above printed "Cycles with two grants: 0" after 1,000,000 cycles with seed 2545F491.
Run the formal task
Run the editor as it is. Read the summary (FAIL at reported step 5), count the steps in the trace and find the three chosen input values in the shaded rows.
Fix the arbiter
On the reload line, replace gnt | pri with hold ? gnt : pri and run again. The result is BMC PASS to depth 20: no failure within 20 cycles of reset, which is a bounded result, not a proof (F1.5).

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module arb3(input clk, rst, input [2:0] req, input [7:0] weight, output reg [2:0] gnt=0);
  reg lock=0;
  reg [1:0] reload=0;
  wire [2:0] pri  = req[0] ? 3'b001 : req[1] ? 3'b010 : req[2] ? 3'b100 : 3'b000;
  wire       hold = lock && |(req & gnt);
  always @(posedge clk) begin
    if (rst) begin gnt<=0; lock<=0; reload<=0; end
    else begin
      lock   <= weight[7];
      reload <= (weight == 8'hA5 && req == 3'b110) ? 2'd1 : (reload == 2'd1 && req == 3'b011) ? 2'd2 : 2'd0;
      if (reload == 2'd2 && req == 3'b111) gnt <= gnt | pri;   // reload cycle: lock holds, encoder grants too
      else gnt <= hold ? gnt : pri;
    end
  end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assert($onehot0(gnt));
  end
endmodule

Check Yourself

Predict the outputThe buggy arb3, sby mode bmc, default depth 20, reset assumed in step 0, smtbmc yices. SBY reports the failing assertion at which step?

module arb3(input clk, rst, input [2:0] req, input [7:0] weight, output reg [2:0] gnt=0);
  reg lock=0;
  reg [1:0] reload=0;
  wire [2:0] pri  = req[0] ? 3'b001 : req[1] ? 3'b010 : req[2] ? 3'b100 : 3'b000;
  wire       hold = lock && |(req & gnt);
  always @(posedge clk) begin
    if (rst) begin gnt<=0; lock<=0; reload<=0; end
    else begin
      lock   <= weight[7];
      reload <= (weight == 8'hA5 && req == 3'b110) ? 2'd1 : (reload == 2'd1 && req == 3'b011) ? 2'd2 : 2'd0;
      if (reload == 2'd2 && req == 3'b111) gnt <= gnt | pri;   // reload cycle: lock holds, encoder grants too
      else gnt <= hold ? gnt : pri;
    end
  end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assert($onehot0(gnt));
  end
endmodule

ConceptWhich claim about the random run is wrong?

The seed decides which path the run takes.Coverage bins count what happened.A longer run raises the odds of hitting the pattern but never reaches certainty.A million cycles with every coverage bin hit means every reachable state was visited.

ConceptWhat does bmc at depth 6 check?

Every state reachable within 6 cycles of reset, for every input sequence of length 6.Every state of the design, reachable or not, for all time, as a prove run would.Six random input sequences chosen with the tool's seed, the way a simulator picks stimulus.The property six times on one trace, once per cycle, the way a simulator checks an assertion.

Read the waveformIn the measured trace, which step is the first where gnt is not one-hot?

The counterexample SBY wrote for the arbiter

Measured with smtbmc yices at depth 20. Three chosen input values in three consecutive cycles, straight after reset.

Step 1, where weight becomes A5Step 4, where gnt is 011Step 5, the last step of the traceStep 2, where lock rises

Remember

A simulation is one path; a million cycles visit at most a million states out of 2^(flops).
BMC at depth k checks every input sequence of length k from reset; the solver returns the breaking inputs as its witness.
Formal checks the property you wrote, within the size it can handle, on the RTL alone.
A BMC PASS names its depth; it is a bounded result, not a proof.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.