Bounded Model Checking

Unroll the design k times, ask the solver at each depth in turn, and read why the first failure is the shortest and why a PASS is bounded.

Lesson: F2.3
Time: 15 min
Runs on: SymbiYosys
Check: 4 questions

A bug needed three bytes to show: a command, a length, then a payload with its top bit set. The bench ran a shallow bound because the block was tiny, and it passed. One more step of depth found the bug on the first run.

The Unrolled Strip

Five copies of seq3, side by side

Copy 0 starts in reset. Each copy takes the next state from the one before it and gets its own free inputs.

rst=1, valid=0, byte_in=0x00
state=CMD, err=0
Reset assumed
No obligation yet
rst=0, valid=1, byte_in=0x00
state=CMD, err=0
!err holds
✓ Holds
rst=0, valid=1, byte_in=0x00
state=LEN, err=0
!err holds
✓ Holds
rst=0, valid=1, byte_in=0x80
state=PAY, err=1
err sampled high
× Fails
rst=0, valid=0, byte_in=0x00
state=CMD, err=0
SBY reports the failure
× Fails

Select a frame to inspect its inputs and assertion.

Measured Yices trace at depth 5. The payload byte 0x80 arrives in PAY at step 3; the clocked check reports step 4.

BMC makes k copies of the design. Copy 0 is held to the initial states. The state of copy i+1 is the next-state function of copy i. Every copy gets its own free inputs. The whole strip, plus "some copy is bad", is one formula for the solver.

One Depth at a Time

Depth 5 is the first bound that reaches the bug

Depth N checks samples 0 to N-2. Depth 4 stops at sample 2; the bug is sampled at 3.

Linear scale. 0 to 20 steps.

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

Measured: depth 3 and 4 PASS, depth 5 FAIL at step 4. The required bound here is the bug's, which nobody knows in advance.

One Solver Question per DepthBMC adds one copy of the design at a time and asks the solver the same question at each depth. Arrows mean "then".

Read the diagram as text

Step 0: reset state bad? UNSAT
Step 1: one copy more: UNSAT
Step 3: the first satisfiable query
Counterexample: the model, written as a trace; reported at step 4
Depth reached, all UNSAT: BMC PASS to that depth, nothing more

Step 0 → Step 1: UNSAT
Step 1 → Step 3: UNSAT ...
Step 3 → Counterexample: SAT
Step 3 → Depth reached, all UNSAT: UNSAT up to the bound

Every shorter length was UNSAT before the solver answered SAT, so the trace is a shortest one. Drawn from the measured log below.

Task	Measured result	Samples checked
depth 3	PASS	samples 0 to 1
depth 4	PASS	samples 0 to 2
depth 5	FAIL at step 4	samples 0 to 3
depth 20	FAIL at step 4	samples 0 to 3

Same design, same solver; only the depth changes.

Measured smtbmc log at depth 5: one assumption check and one assertion check per step, in order.

Checking assumptions in step 0..
Checking assertions in step 0..
Checking assumptions in step 1..
Checking assertions in step 1..
Checking assumptions in step 2..
Checking assertions in step 2..
Checking assumptions in step 3..
Checking assertions in step 3..
Checking assumptions in step 4..
Checking assertions in step 4..
BMC failed!
Assert failed in seq3: design.sv:12.35-12.47 (_witness_.check_design_sv_12_assert_16)
Status: failed

The solver is asked about step 0, then step 1, then step 2, and stops at the first satisfiable query. Every shorter length was already UNSAT, so the trace it prints is a shortest one. At depth 20 the measured result is still FAIL at step 4.

Read the Counterexample

Measured counterexample, depth 5: reset at step 0, three bytes at steps 1 to 3, err sampled at 3, reported at 4.

The trace is the solver's model: one column per copy. Only the inputs are chosen; the state follows from them. The payload byte at step 3 is the one the bug needs.

The rule in concurrent SVA

assert property (@(posedge clk) disable iff (rst)
  !err);

err must never rise outside reset.

What the engine runs

always @(posedge clk) if (!rst) assert(!err);

A clocked immediate assertion, sampled at each edge.

When Is a Bound a Proof?

Every reachable state is two steps from reset

The fixed seq3 has three reachable states. The fourth state value, 3, is never reached.

The diameter is 2, so a bound past it has seen every reachable state. The tool cannot know that: prove mode on the fixed design returned UNKNOWN, starting from state 3.

Read the states and transitions

CMD: initial, depth 0.
LEN: reachable, depth 1.
PAY: reachable, depth 2.
3: unreachable, depth 0.
err: bad, depth 1.
CMD → LEN.
LEN → PAY.
PAY → CMD.
3 → err (induction candidate).

Illustration. Drawn from the RTL. The measured induction start state is the unreachable state 3 (F2.4).

If every reachable state is within d steps of reset, BMC at a depth past d has seen them all, and a PASS is a proof. That d is the diameter of the state graph. Computing it is as hard as the proof, and a 32-bit counter has a diameter of 2^32 − 1.

So read a BMC PASS as "no failure in samples 0 to 18", never more. Unbounded proofs need induction (F2.4) or IC3 (F2.5).

What Grows with Depth

Measured sweepTime Grows with the BoundWhole-task time on this machine for the fixed seq3 and for fifo16, both passing.

seq3
fifo16

Read the plot as a table

Depth	seq3	fifo16
5	493 ms	520 ms
10	493 ms	514 ms
15	514 ms	771 ms
20	515 ms	2.318 s
25	533 ms	7.281 s

Measured with smtbmc yices. At depth 30 fifo16 hit the 20 s time limit: no verdict.

Each extra step adds one more copy of the logic, so the formula grows linearly. The time does not: fifo16 has wide pointers and a memory, and its solve time climbs much faster than seq3, which has two state bits.

Engine at depth 5	Result	Time
`smtbmc yices`	FAIL at step 4	0.2 s
`abc bmc3`	FAIL at step 4	0.3 s

Measured with SBY called directly. Same shortest step from a word-level and a bit-level engine.

Asked in Interviews

Question	Answer
What is BMC? Why does it find the shortest counterexample?	Unroll k copies and ask the solver at each depth in order. It stops at the first satisfiable depth, so no shorter trace exists.
Why is BMC not a proof?	A bug may need more steps than the bound. A PASS is a proof only past the diameter, which is unknown.
What grows with depth?	The formula grows with each copy; solve time grows faster, and depends on the design.

Try It

The lab runs seq3 at depth 5 with smtbmc yices. Measured: FAIL at step 4.

Walk the depth
Set the depth to 3, then 4, then 5. Read each summary and the samples it checked.
Go deep
Set depth 20. The trace still ends at step 4: the bound is not the trace length.
Fix and ask again
Replace state == PAY && byte_in[7] with state == 2'd3. Depth 20 passes. Is that a proof? Switch the mode to prove and read the answer.

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 seq3(input clk, rst, valid, input [7:0] byte_in, output err);
  localparam CMD = 2'd0, LEN = 2'd1, PAY = 2'd2;
  reg [1:0] state=CMD;
  // err must never rise: no byte may confuse the detector
  assign err = valid && state == PAY && byte_in[7];
  always @(posedge clk)
    if (rst) state <= CMD;
    else if (valid) state <= state == CMD ? LEN : state == LEN ? PAY : CMD;
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) assert(!err);
endmodule

Check Yourself

Predict the outputseq3 with the bug, mode bmc, depth 20, smtbmc yices, reset assumed in step 0. SBY reports the failure at step:

module seq3(input clk, rst, valid, input [7:0] byte_in, output err);
  localparam CMD = 2'd0, LEN = 2'd1, PAY = 2'd2;
  reg [1:0] state=CMD;
  // err must never rise: no byte may confuse the detector
  assign err = valid && state == PAY && byte_in[7];
  always @(posedge clk)
    if (rst) state <= CMD;
    else if (valid) state <= state == CMD ? LEN : state == LEN ? PAY : CMD;
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) assert(!err);
endmodule

ConceptWhich statement about BMC is wrong?

The formula grows with the depth.Each copy of the design has its own free inputs.The first satisfiable step gives a shortest counterexample.BMC at depth 20 proves the property for all time.

ConceptWhen is a BMC PASS at depth k a proof?

When k is at least the diameter of the reachable state graph.Never: a bounded run cannot be a proof of anything at all.When k is 20, the default depth of an SBY task, or more.When k is at least the number of flops in the cone of the property.

Read the waveformIn the measured trace, at which step does the input the bug needs arrive?

Measured counterexample, depth 5: reset at step 0, three bytes at steps 1 to 3, err sampled at 3, reported at 4.

Step 2Step 3Step 1Step 4

Remember

BMC unrolls k copies and asks the solver about each depth in order.
The first satisfiable depth gives a shortest counterexample.
Depth N checks clocked samples 0 to N-2; a PASS covers only those.
A bound is a proof only past the diameter, which nobody knows for a real design.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.