← Formal Verification Interviews
Interview Question · Debug
A Proof That Will Not Converge
- Likely at AMD
- Likely at Intel
- Likely at Qualcomm
The Question
The interviewer asks
An assertion on a watchdog block has run for hours with no answer. Walk me through what you do.
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
First work out which of three causes it is. The depth needed is huge, the cone holds hard logic such as a multiplier, or the property is not inductive. Read the cone and the engine log rather than guessing. Then change the question to match. Abstract the counter, cut datapath the property does not read, add helper invariants, split cases or switch engines. Every reduction gets a written reason and a rerun of a known-buggy version.
Read the diagram as text
- pre, ticks: captured at start, each at least 256
- pre_q × ticks_q: 16 × 16 multiplier
- timer: 32-bit counter, cleared by a kick
- expired: timer == product: the cut point
- kick, start: free inputs
- state: IDLE, RUN, BARK
- assertion: kick in RUN |=> !bark
- pre, ticks → pre_q × ticks_q
- pre_q × ticks_q → expired
- timer → expired
- expired → state: cut here
- kick, start → state
- kick, start → timer: clears
- state → assertion
Every block drawn is in the cone. Yosys keeps 67 flop bits after prep; with expired cut, 3. The depth the timer adds is what no bound reaches.
What changing the question looks like, measured in lesson F4.1: with the expiry comparator freed, the same bmc run fails at step 4 in about half a second. A kick and a free expired arrive together, and the dog still barks.
Measured counterexample with the timer cut (bmc, depth 20): FAIL at step 4, 0.5 s. expired is now a free input, shaded like the others.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Mid-Level)
A good mid-level answer names the three causes: depth, hard logic and properties that are not inductive. It matches each cause to a technique.
What Interviewers Listen For (Senior)
A good senior answer plans convergence up front, with design-for-formal requests and an engine-time budget per property. It tracks open UNKNOWNs as risks. It accepts a justified bounded result where a full proof costs too much.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompareScale It
- A Proof That Will Not Converge
-
WhyWhy a Wide Counter Defeats BMCL1 JuniorL2 Mid-Level
Why does a 16-bit timeout counter make a bounded proof hopeless, and what do you do 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
Reaching expiry from reset takes as many steps as the count. BMC must unroll every one of them, so the required depth runs into the tens of thousands. Instead, abstract the counter to the few values that matter and prove the abstraction on the real counter in a side run. A one-transition property can also be proven by induction at full width without ever reaching expiry.
Where the Bug Lives on the Real Timer, and Where Depth 40 StopsThe faulty watchdog's counterexample on the real timer: reset, start, 65,536 cycles of counting, then the kick that lands on the expiry. Depth 40 checks samples 0 to 38. Read the diagram as text
- step 0: reset: assumed
- step 1: start: pre and ticks captured, each at least 256
- steps 2 to 65,537: RUN: timer counts 0 to 65,535
- step 65,538: kick on expiry: the faulty FSM tests the expiry first
- step 65,539: bark: the violation; reported at step 65,540
- depth 40 ends at sample 38: required depth: 65,541
- step 0: reset → step 1: start
- step 1: start → steps 2 to 65,537
- steps 2 to 65,537 → step 65,538: kick on expiry
- step 65,538: kick on expiry → step 65,539: bark
- depth 40 ends at sample 38 → steps 2 to 65,537: stops inside the wait
Depth 40 covers 0.06 % of the bound the bug needs. The steps on the real timer follow from the measured cut trace plus 65,536 counting cycles.
Self-Check
Tick each key point you covered in your answer.
-
What IfIs the Abstract Counter SoundL2 Mid-LevelL3 Senior
You replace the 16-bit timeout counter with an abstract one that may expire at any time. Why is that sound, and what can it break?
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 abstract counter can do everything the real one does, plus more, such as expiring early. So a pass on the abstract model holds for the real design. The extra behaviour can cause false failures, for example an early timeout. Check each failure against the real counter, and prove the values you kept on the real design.
Self-Check
Tick each key point you covered in your answer.
Half-Truth
"The abstract model passes, so the real counter needs no checks."
The abstraction is sound only if it includes every real count sequence. Prove the values it keeps, such as reset and expiry, on the real counter.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 10 "Counter abstraction"
-
CompareBlackbox vs Cut PointL2 Mid-Level
Compare blackboxing a submodule with placing a cut point.
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 blackbox turns every output of a module into a free input. That suits memories and arithmetic the property does not depend on. A cut point frees a single internal node. So you can remove one hard cone, such as a CRC check, without dropping the module around it. Both add behaviour, so a pass stays sound and a failure must be checked at the freed signal.
Self-Check
Tick each key point you covered in your answer.
-
What IfCase Splitting a Hard ProofL2 Mid-LevelL3 Senior
What if a property is hard only for some opcodes or address ranges? How do you split it safely?
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
Run the proof once per case, each with an assumption that pins the case variable. Prove separately that the cases together cover every value. Pin the case for the whole run, from a value fixed at the start. A split that lets the case change each cycle can hide interleavings between cases. The slow case then shows you where the hard logic is.
One Proof Becomes ThreeThe assertion is proved once per burst type. The three cases together are every legal burst, because the request never carries burst type 3. Read the diagram as text
- every legal burst: FIXED, INCR or WRAP, any order
- case FIXED: busy && burst_q == FIXED |-> in page
- case INCR: busy && burst_q == INCR |-> in page
- case WRAP: busy && burst_q == WRAP |-> in page
- union: the three conditions cover every busy cycle
- every legal burst → case FIXED
- every legal burst → case INCR
- every legal burst → case WRAP
- case FIXED → union
- case INCR → union
- case WRAP → union
Soft split: the case is the assertion’s condition, so each run still allows any sequence of bursts.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F4.3.1: An Exhaustive Address Case SplitSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Prove ItSolve F4.1.1: Cut the Watchdog ConeSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Scale ItGetting Designers to Build for FormalL3 SeniorL4 Staff
As formal lead, how do you get designers to make their blocks cheaper to prove?
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
Agree on a few habits before RTL is written. These are right-sized state, control separated from data, parameterised timers and depths, one reset, and important state exposed or named. Show one measured before-and-after from your own project, because that persuades more than a rule. Designers who run formal on fresh RTL also find bugs while they still remember the code.
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.
Missed Corner
"BMC at depth 20 passed, so the watchdog is fine."
Expiry needs at least 65,536 cycles here, so depth 20 never sees it. Freeing the expiry comparator exposes the real bug, a kick on the expiry cycle that still barks, at step 4.
Run It
The watchdog from lesson F4.1: the timeout is pre * ticks, each at least 256.
module wdt(input clk, rst, start, kick, input [15:0] pre, ticks, output bark);
localparam IDLE = 2'd0, RUN = 2'd1, BARK = 2'd2;
reg [1:0] state = IDLE;
reg [15:0] pre_q = 0, ticks_q = 0;
reg [31:0] timer = 0;
wire expired = timer == pre_q * ticks_q;
assign bark = state == BARK;
always @(posedge clk)
if (rst) begin state <= IDLE; timer <= 0; end
else case (state)
IDLE: if (start) begin pre_q <= pre; ticks_q <= ticks; timer <= 0; state <= RUN; end
RUN: if (expired) state <= BARK; // bug: expiry tested first
else if (kick) timer <= 0;
else timer <= timer + 32'd1;
default: if (kick) state <= IDLE;
endcase
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(*) assume(pre >= 16'd256 && ticks >= 16'd256); // the shortest timeout
// a kick while running means no bark in the next cycle
reg f_kick = 0;
always @(posedge clk) begin
f_kick <= !rst && state == RUN && kick;
if (!rst && f_kick) assert(!bark);
end
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
See the Fix
module wdt(input clk, rst, start, kick, input [15:0] pre, ticks, output bark);
localparam IDLE = 2'd0, RUN = 2'd1, BARK = 2'd2;
reg [1:0] state = IDLE;
reg [15:0] pre_q = 0, ticks_q = 0;
reg [31:0] timer = 0;
wire expired = $anyseq; // cut point: any value, every cycle
assign bark = state == BARK;
always @(posedge clk)
if (rst) begin state <= IDLE; timer <= 0; end
else case (state)
IDLE: if (start) begin pre_q <= pre; ticks_q <= ticks; timer <= 0; state <= RUN; end
RUN: if (expired) state <= BARK; // bug: expiry tested first
else if (kick) timer <= 0;
else timer <= timer + 32'd1;
default: if (kick) state <= IDLE;
endcase
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
always @(*) assume(pre >= 16'd256 && ticks >= 16'd256); // the shortest timeout
// a kick while running means no bark in the next cycle
reg f_kick = 0;
always @(posedge clk) begin
f_kick <= !rst && state == RUN && kick;
if (!rst && f_kick) assert(!bark);
end
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 4
Half-Truth
"Give it a bigger machine and a longer timeout."
State space grows exponentially with the flops in the cone. Without changing the question you usually buy hours, not an answer.
Misconception
"The block is small, so its proof should be easy."
Convergence depends on what is in the property's cone, not on gate count. One 16-bit timer can push the required depth into the tens of thousands.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 10 "Design state and associated complexity"; ASIC Point lesson F4.1 (required depth 65,541, measured)