← Formal Verification Interviews
Interview Question · Debug
When k-Induction Returns UNKNOWN
- Likely at Arm
The Question
The interviewer asks
Your prove run passes the base case but the induction step fails, so the tool reports UNKNOWN. Is there a bug, and what do you do next?
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
Not necessarily a bug. The induction step may start from any state where the property held for k cycles, including states reset never reaches. Read step 0 of the induction trace and name what is impossible about it. Assert that relation as a helper and rerun until the step passes. Raising k may never close the proof, while one good helper often does.
No reset in this run. The solver picks the first state, keeps the property true for 11 samples, then breaks it.
wr=0, rd=0, rst=0
count=1, wr_ptr=0, rd_ptr=15Assumed true (not empty)
Assumed for inductionwr=0, rd=0, rst=0
count=1, wr_ptr=0, rd_ptr=15Assumed true (not empty)
Assumed for inductionwr=0, rd=0, rst=0
count=1, wr_ptr=0, rd_ptr=15Assumed true (not empty)
Assumed for inductionwr=0, rd=0, rst=0
count=1, wr_ptr=0, rd_ptr=15Assumed true (not empty)
Assumed for inductionwr=0, rd=1, rst=0
count=1, wr_ptr=0, rd_ptr=15Assumed true (not empty)
Assumed for inductionwr=0, rd=0, rst=0
count=0, wr_ptr=0, rd_ptr=16empty, pointers differ
× Failswr=0, rd=0, rst=0
count=0, wr_ptr=0, rd_ptr=16SBY reports the failure
× Fails
Select a frame to inspect its inputs and assertion.
Measured trace_induct.vcd, frames 0, 1, 2, 9, 10, 11, 12 of 13. The FIFO idles until step 10, then one read empties it with the pointers apart.
Reachable states keep count equal to wr_ptr - rd_ptr. The induction start breaks that relation, and one read from it is bad.
Measured start: count = 1, wr_ptr = 0, rd_ptr = 15, so wr_ptr − rd_ptr = 17 (mod 32). The helper count == wr_ptr - rd_ptr is false there, so it cuts this state off.
Read the states and transitions
- c=0: initial, depth 0.
- c=1: reachable, depth 1.
- c=2: reachable, depth 2.
- c=1: unreachable, depth 0.
- bad: bad, depth 1.
- c=0 → c=1.
- c=1 → c=0.
- c=1 → c=2.
- c=2 → c=1.
- c=1 → bad (induction candidate).
Illustration. Reachable count values drawn for 0 to 2 only. The unreachable state is the measured induction start.
The log that starts the conversation, measured on the 16-entry FIFO in lesson F2.4: the base case passed, the induction step did not.
summary: engine_0 (smtbmc yices) returned pass for basecase
summary: engine_0 (smtbmc yices) returned FAIL for induction
summary: counterexample trace [induction]: job/engine_0/trace_induct.vcd
summary: failed assertion top._witness_.assert_top_sv_20_assert_30 at top.sv:20.16-20.40
DONE (UNKNOWN, rc=4)Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Junior)
A good junior answer says UNKNOWN is not a FAIL. It says the induction trace can start in a state that reset never reaches, and suggests a helper assertion.
What Interviewers Listen For (Senior)
A good senior answer reads step 0 carefully and keeps only the helpers the proof needs. It reruns a faulty twin to show the helpers hide nothing. It moves to PDR, an engine that builds its own invariant, when helpers get expensive.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompareScale It
- When k-Induction Returns UNKNOWN
-
WhyWhy the Induction Step Starts AnywhereL1 JuniorL2 Mid-Level
Why can the induction step start in a state the design never reaches from reset?
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 step only assumes the property held for k consecutive cycles; it says nothing about reachability. A state can satisfy the property but break a hidden invariant, such as two equal counters being unequal. Such a state is a legal start. The fix is to make the hidden invariant part of what is proven, so those states are ruled out.
Two Runs Make One ProofThe base case is a BMC from reset. The step drops reset and asks whether k good states can be followed by a bad one. Read the diagram as text
- Base case: copy 0 held to reset
- k copies from reset: property checked in every copy
- basecase PASS: BMC to depth k finds nothing
- Induction step: copy 0 is any state
- k copies assumed good: the property holds in each
- copy k+1: property must hold here too
- Base case → k copies from reset
- k copies from reset → basecase PASS
- Induction step → k copies assumed good
- k copies assumed good → copy k+1: one more step
Both pass: the property holds in every reachable state. Base passes and step fails: UNKNOWN.
Self-Check
Tick each key point you covered in your answer.
-
What IfRaising k Instead of Writing a HelperL2 Mid-Level
What if you simply raise k instead of writing a helper? When does that work, and when does it never work?
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
Raising k makes the step assume the property held for more cycles. That works only when every bad start state reaches a failure within k cycles. Two counters that must stay equal can drift apart and stay apart for any number of cycles. Then no k closes the proof; only a helper that states the invariant does.
Self-Check
Tick each key point you covered in your answer.
Misconception
"UNKNOWN at k = 20, so try k = 200."
If an unreachable state can satisfy the property for any number of cycles, a larger k only moves the start. Read step 0 and write the helper.
Source Lesson F2.4 key points
-
CompareIC3/PDR vs k-InductionL2 Mid-Level
Asked if they mention other engines
Compare k-induction (an induction proof over k steps) with IC3/PDR on a FIFO proof that k-induction cannot close.
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
IC3/PDR does not unroll but keeps frames of clauses. It proves each clause relative to the previous frame until two frames match, giving an inductive invariant it built itself. On the lesson's 16-entry FIFO, PDR proves the property with no helpers while k-induction stays UNKNOWN at k = 12. Its counterexamples start at reset but need not be the shortest. No engine wins everywhere, so teams race several.
module fifo16(input clk, rst, wr, rd, input [7:0] wdata, output [7:0] rdata, output empty, full); reg [7:0] mem [0:15]; reg [4:0] wr_ptr=0, rd_ptr=0, count=0; assign empty = count == 5'd0; assign full = count == 5'd16; wire do_wr = wr && !full, do_rd = rd && !empty; assign rdata = mem[rd_ptr[3:0]]; always @(posedge clk) if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end else begin if (do_wr) begin mem[wr_ptr[3:0]] <= wdata; wr_ptr <= wr_ptr + 5'd1; end if (do_rd) rd_ptr <= rd_ptr + 5'd1; count <= count + do_wr - do_rd; end always @(posedge clk) begin if ($initstate) begin assume(rst); end else begin assume(!rst); end end always @(posedge clk) if (!rst) begin if (empty) assert(wr_ptr == rd_ptr); end endmodulePrints:
prove, depth 12 (abc pdr): PASSSelf-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F2.5.1: Let the Engine Find the InvariantSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Prove ItSolve F2.4.1: Close the Induction with a HelperSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Scale ItKeeping Helper Invariants HonestL3 Senior
A large proof now has thirty helper assertions. How do you keep them from becoming a liability?
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
Every helper is asserted, so it is proven, never assumed. Keep only the helpers the final proof needs, by removing them one at a time and rerunning. After each change, rerun a faulty version of the design to show the set still catches the bug. Review helpers like RTL, because they become the next engineer's spec of the block.
The Strengthening LoopRun prove; on UNKNOWN read step 0 of the induction trace, name the relation it breaks, assert that relation, and run again. Finish with the faulty twin. Read the diagram as text
- run prove: k-induction, small depth
- read step 0: the induction trace starts anywhere
- name what is impossible: a relation reset always keeps and step 0 breaks
- assert it: a helper, proven in the same run
- PASS: then run the faulty twin: it must still fail
- run prove → read step 0: UNKNOWN
- read step 0 → name what is impossible
- name what is impossible → assert it
- assert it → run prove: again
- run prove → PASS: base and step pass
A helper is an assertion, never an assumption. An assumed helper would hide every state that breaks it, real bugs included.
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
"UNKNOWN means there is a bug the tool could not show."
Here a and b always step together, so the design is correct. The induction step starts with them unequal and fails; asserting a == b closes the proof at k = 2.
Run It
Two counters that always move together; the property only mentions their value 10.
module ab_cnt(input clk, rst, en);
reg [3:0] a=0, b=0;
always @(posedge clk)
if (rst) begin a <= 0; b <= 0; end
else if (en) begin a <= a + 4'd1; b <= b + 4'd1; end
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
assert(a != 4'd10 || b == 4'd10);
end
endmodule
Prints: prove, depth 2 (smtbmc yices): UNKNOWN
See the Fix
module ab_cnt(input clk, rst, en);
reg [3:0] a=0, b=0;
always @(posedge clk)
if (rst) begin a <= 0; b <= 0; end
else if (en) begin a <= a + 4'd1; b <= b + 4'd1; end
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(posedge clk) if (!rst) begin
assert(a != 4'd10 || b == 4'd10);
assert(a == b); // helper
end
endmodule
Prints: prove, depth 2 (smtbmc yices): PASS
Misconception
"Assume the helper instead of asserting it; it runs faster."
An assumed helper is never checked, so a wrong one silently removes real behaviour. Prove it as an assertion first; only then may it constrain later proofs.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 10 "Writing custom helper assumptions", "Leveraging proven assertions"
Half-Truth
"Keep raising k until it passes."
In the lesson the 16-entry FIFO stays UNKNOWN at k = 12 and at k = 16, yet passes at k = 2 once helpers are asserted. Depth rarely beats a missing invariant.