← Formal Verification Interviews
Interview Question · Concept
What a Bounded Pass Promises
The Question
The interviewer asks
The tool reports BMC PASS at depth 20 on an idle-timeout block. Your manager asks whether the block is verified. What do you say?
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
It means no input sequence breaks the property within the first 20 steps from reset, and nothing more. A bug that needs a longer run, such as a counter reaching its limit, is invisible at that depth. Either compute the depth the logic needs and show covers reach it, or run a prove mode for an unbounded answer.
Depth 20 checks clocked samples 0 to 18 and passes. The violation is sampled state 26, reported at step 27. Depth 28 is the smallest bound that sees it (samples 0 to 26).
Linear scale. 0 to 32 steps.
- Checked bound
- 20
- Required bound
- 28
- First reported failure
- 27
- Claim
- Counterexample found
Depth 20 passes, yet the bug sits at step 27. A bounded pass says nothing beyond its depth.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Fresher)
A good fresher answer says a BMC (bounded model checking) pass holds only up to a depth. It always quotes the depth with the result, and knows a deeper bug can hide.
What Interviewers Listen For (Senior)
A good senior answer works out the required depth from the counters and transaction lengths that feed the property. It shows that covers reach that depth, and reports bounded results as bounded at sign-off.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyProve ItBreak ItCompareScale It
- What a Bounded Pass Promises
-
WhyWorking Out the Required DepthL2 Mid-LevelL3 Senior
How do you work out the depth a bounded proof must reach before you trust it?
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
Start from the deepest counter in the property's cone, the longest transaction and the property's own window. Then add the tool's step offset. Check the number with covers: the deepest interesting behaviour must be reached inside the bound. The book's guideline is to prove assertions deeper than the longest cover trace, ideally about twice as deep.
TMO = 12: the bound stops short Depth 12 against the required depth 17 of the TMO = 12 block with the late-error bug.
Linear scale. 0 to 20 steps.
×- Checked bound
- 12
- Required bound
- 17
- First reported failure
- 16
- Claim
- Counterexample found
Measured: depth 12 gives BMC PASS to depth 12; depth 20 gives FAIL at reported step 16. The bound stopped short.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F1.5.1: How Deep Is the Expiry Corner?Simulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Break ItA Required Depth That Was Too SmallL2 Mid-LevelL3 Senior
You computed a required depth of 30 and proved to 30. How can the result still miss a bug?
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 number is only as good as its inputs. A counter you missed in the cone, a longer transaction or a wrong step offset makes 30 too small. Covers check it: the deepest interesting state must be reached inside the bound. A depth sweep, where a planted bug fails near the predicted depth, also checks the arithmetic.
Self-Check
Tick each key point you covered in your answer.
Missed Corner
"All my covers hit by depth 12, so depth 30 is plenty."
Covers only show the states you wrote covers for. A counter with no cover can need far more steps, so list every counter in the cone first.
Source Lesson F7.3 key points
-
CompareBMC vs Prove Mode, and What UNKNOWN MeansL1 JuniorL2 Mid-Level
Asked if they suggest switching to prove mode
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.
-
Scale ItBounded Proofs at Sign-OffL3 Senior
Your full proofs will not converge before tape-out. Can you sign off with bounded proofs instead?
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 the bound is argued, not hoped. The page must show the required depth from the counters and transactions, and a run that reaches it. It must also show covers of the deepest behaviour inside the bound. The page reports the result as bounded, with the depth, the tool version and the date. It also states the risk of a deeper bug.
Self-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
"PASS is PASS; the depth is just a tool setting."
This idle counter expires at 24, and the bug needs a start on the expiry cycle. Depth 20 passes; depth 28 fails at step 27.
Run It
The idle timer from lesson F1.5, whose bug needs 27 steps from reset.
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);
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
See the Fix
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);
endmodule
Prints: bmc, depth 28 (smtbmc yices): FAIL at step 27
Missed Corner
"At depth 20 every cycle up to 20 is checked."
Tools count differently. In this flow depth N checks clocked samples 0 to N-2, and the reported step is the sample plus one. Know your tool's convention before you quote a bound.
Source ASIC Point lesson F2.3, measured on SBY v0.70-9
Half-Truth
Raises the depth until the run times out and calls the last pass a proof.
A bound is a proof only past the design's diameter, the most steps any reachable state needs from reset. Nobody knows it for a real design. Use a prove mode, or justify the bound with covers.