← Formal Verification Interviews
Interview Question · Concept
How Bounded Model Checking Works
The Question
The interviewer asks
How does bounded model checking work, and in its solver query, which answer is the good news?
You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
BMC unrolls the design k times from the initial state. It asks a SAT or SMT solver whether some input assignment reaches a bad state at any step. Satisfiable means yes, and the assignment is the counterexample trace. Unsatisfiable means no trace of that length breaks the property, which is the good news. Depths are tried in order, so the first failure found is a shortest one.
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.
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=0Reset assumed
No obligation yetrst=0, valid=1, byte_in=0x00
state=CMD, err=0!err holds
✓ Holdsrst=0, valid=1, byte_in=0x00
state=LEN, err=0!err holds
✓ Holdsrst=0, valid=1, byte_in=0x80
state=PAY, err=1err sampled high
× Failsrst=0, valid=0, byte_in=0x00
state=CMD, err=0SBY 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.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Fresher)
A good fresher answer describes unrolling the design and the single solver question. It says SAT means a counterexample and UNSAT means a pass for that depth.
What Interviewers Listen For (Mid-Level)
A good mid-level answer explains why the first failure found is the shortest, and what the bound does not promise. It says when a word-level SMT solver beats bit-blasting.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompare
- How Bounded Model Checking Works
-
WhyWhy the First BMC Failure Is the ShortestL1 Junior
Why is the first counterexample BMC returns guaranteed to be a shortest one?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
The checker asks about depth 1, then 2, then 3, and stops at the first depth the solver finds satisfiable. If a shorter failing trace existed, an earlier query would already have been satisfiable. That makes BMC traces short and easy to read, which is one reason engineers run bmc for bug hunting.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F2.3.1: Three Bytes Before the Bad StateSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
CompareSAT vs SMT Solvers for DatapathsL2 Mid-Level
When does a word-level SMT solver help over a bit-level SAT engine?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
A SAT engine sees only gates, so a wide adder or multiplier becomes thousands of clauses. An SMT solver keeps words and arithmetic as theories and can simplify before it falls back to bits. The verdict is the same either way; only the time differs, and in the lesson the winner changed with the property.
Measured sweepThe Same Multiplier, Wider Each TimeBMC of mul_saat depth W + 4, which covers one full multiplication. Whole-task time with SBY on this machine.- smtbmc yices
- smtbmc boolector
- smtbmc z3
- abc bmc3
Read the plot as a table
Operand width smtbmc yices smtbmc boolector smtbmc z3 abc bmc3 4 189 ms 189 ms 205 ms 176 ms 4.5 256.8 ms 246.3 ms 338 ms 280.3 ms 5 324.5 ms 303.5 ms 471 ms 384.5 ms 5.5 392.3 ms 360.8 ms 604 ms 488.7 ms 6 460 ms 418 ms 737 ms 593 ms 6.5 1.293 s 703.5 ms 1.794 s 1.445 s 7 2.127 s 989 ms 2.852 s 2.297 s 7.5 6.319 s 2.285 s 9.634 s 10.75 s 8 10.51 s 3.582 s 16.42 s 19.2 s Measured once per point. Single runs on one machine are not a ranking.
Self-Check
Tick each key point you covered in your answer.
-
What IfBMC and the Design DiameterL2 Mid-LevelL3 Senior
What if you knew the design's diameter, the most steps any reachable state needs from reset? Would BMC then give a full proof?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
Yes: if every reachable state can be reached within d steps, a BMC pass to that depth covers every reachable state. The problem is that nobody knows the diameter of a real design, and it grows with every counter. That is why full proofs use induction or IC3/PDR, an engine that builds its own invariant. Bounded results are argued from a required depth instead.
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:
provemode 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 of the lesson's small sequence detector.
Self-Check
Tick each key point you covered in your answer.
-
What IfBMC vs Prove Mode, and What UNKNOWN MeansL1 JuniorL2 Mid-Level
What does a prove mode give you that BMC does not, and what does an UNKNOWN result mean?
2:30You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.
Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
You can edit your answer before you send it. Feedback uses AI and checks your answer only against our written answer. No credits are used and your answer is not saved.
Reveal the Model Answer
Prove mode runs k-induction (an induction proof over k steps) or IC3/PDR (an engine that builds its own invariant). It can return a PASS that holds for all time. UNKNOWN means the base case passed but the induction step did not, so no proof has been found. It is an open item, never a pass, and it can sit on a real bug deeper than the base case. On the buggy idle timer here, prove at k = 2 reports UNKNOWN rather than FAIL.
module seq25(input clk, rst, busy, start, output expired, output reg [1:0] phase=0); reg [4:0] idle_cnt=0; assign expired = idle_cnt == 5'd24; always @(posedge clk) begin if (rst) begin idle_cnt<=0; phase<=0; end else begin if (busy) idle_cnt <= 0; else if (expired && !start) idle_cnt <= 0; // bug: start on the expiry cycle skips the clear else idle_cnt <= idle_cnt + 5'd1; if (expired) phase <= start ? 2'd3 : 2'd0; else if (start) phase <= phase + 2'd1; end end always @(posedge clk) begin if ($initstate) begin assume(rst); end else begin assume(!rst); end end always @(posedge clk) if (!rst) assert(idle_cnt <= 5'd24); endmodulePrints:
prove, depth 2 (smtbmc yices): UNKNOWNSelf-Check
Tick each key point you covered in your answer.
What People Get Wrong
Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.
Misconception
"SAT means the property is satisfied, so it passed."
The solver is asked whether a bad trace exists. SAT means it found one; a pass is UNSAT at every depth checked.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 2 "Bounded model checking"; Biere, Cimatti, Clarke, Zhu, TACAS 1999
Missed Corner
"A bug at step 4 shows up at depth 4."
In this flow depth N checks samples 0 to N-2 and reports the step as sample plus one. The lesson's bug at step 4 passes depth 4 and fails at depth 5.
Run It
A three-state packet parser that raises err on a third valid byte with bit 7 set, run at depth 4.
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
Prints: bmc, depth 4 (smtbmc yices): PASS
See the Fix
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
Prints: bmc, depth 5 (smtbmc yices): FAIL at step 4
Half-Truth
"Use the largest depth the tool allows; deeper always finds more."
Each step enlarges the formula. Past the required depth the extra time buys nothing, and a timeout returns no answer at all.