← Formal Verification Interviews
Interview Question · Waveform
Reading a Formal Counterexample
The Question
The interviewer asks
A formal run fails at step 7 and hands you a trace. How do you read it, and how do you tell a real bug from a problem in your bench?
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
Start at the failing step and walk backwards to the first value that set the design on the wrong path. Then sort the cause into one of four: an RTL bug, a missing assumption, a wrong property, or reset not modelled. The state at step 0 and the inputs the solver chose usually decide it. An input sequence the real environment never produces calls for an assumption, not an RTL change.
Read the diagram as text
- FAIL at step n: walk back to the cause
- Step 0 legal?: could a reset produce it
- Shaded inputs legal?: would the spec allow them
- Check matches the spec?: is the property too strict
- Model the reset: assume rst in step 0
- Add an assumption: on the input, from the spec
- Fix the property: the spec row, as written
- RTL bug: legal start, legal inputs, right check
- FAIL at step n → Step 0 legal?
- Step 0 legal? → Shaded inputs legal?: yes
- Shaded inputs legal? → Check matches the spec?: yes
- Step 0 legal? → Model the reset: no
- Shaded inputs legal? → Add an assumption: no
- Check matches the spec? → Fix the property: no
- Check matches the spec? → RTL bug: yes
Only when the start state, the inputs and the check are all right is the trace a bug in the RTL.
The measured trace from lesson F1.4, read backwards: the check fails at step 7 because ack is built from the delayed pending_d, still high one cycle after the abort at step 4 cleared pending.
Measured: FAIL at reported step 7, 629 ms, depth 20, smtbmc yices. Reset is assumed in step 0.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Fresher)
A good fresher answer reads the trace backwards from the failing step. It can name the four possible causes of a failure.
What Interviewers Listen For (Mid-Level)
A good mid-level answer first checks step 0, and each input the solver chose, against the spec. It writes the missing assumption from a spec row. Then it covers what that assumption might exclude.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItCompareScale It
- Reading a Formal Counterexample
-
WhyWhy Formal Traces Are ShortL1 Junior
Why are formal counterexamples usually much shorter than the simulation failures for the same 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
BMC checks depth 1, then 2, and so on, and stops at the first satisfiable depth, so no shorter failing trace exists. The solver also chooses every input directly instead of waiting for random stimulus to line up. An IC3/PDR counterexample (from the engine that builds its own invariant) starts at reset too but need not be the shortest.
Self-Check
Tick each key point you covered in your answer.
-
What IfA Failure One Step After ResetL1 Junior
Asked if the trace fails right after reset
Your counterexample fails at step 1, before any request has arrived. What do you check first?
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
Check how the design starts. A failure that early usually has one of two causes. Either reset was not assumed in the first step, or a flop with no reset started at a value the solver chose. Look at step 0. If a register holds a value reset would never give it, fix the bench or add the reset, not the logic.
Lesson F1.4's Trace B: with no reset assumption,
ackis already high at step 0 whilepending_qis low, so the check fails at once.Trace B: the same check with no reset assumption Measured: FAIL at reported step 1, 601 ms. The failing state is step 0 itself. F1.6 is about this.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F1.4.2: A Failure Before the First RequestSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfA Register That Firmware InitialisesL1 JuniorL2 Mid-Level
What if the unreset register is set by firmware at boot, so the hardware team refuses to add a 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
Then the start value is an assumption, not a fact. Write it as an initial-state assumption that the register holds its boot value. Put it on the sign-off list, so someone checks it against the boot code. Add a cover that the block still runs, so the assumption did not empty the bench.
Self-Check
Tick each key point you covered in your answer.
Missed Corner
"Firmware sets it, so formal can ignore that register."
Left free, the solver starts it at any value and reports false failures. Fixed without a note, the proof hides the case where firmware forgets.
Source Lesson F1.6 key points
-
Prove ItSolve F1.4.1: The Acknowledgement After CancellationSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
CompareDebugging a Counterexample vs a Simulation FailureL1 JuniorL2 Mid-Level
Compare debugging a formal counterexample with debugging a failing random simulation.
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 simulation failure is one run, often thousands of cycles long, with the cause buried somewhere in the middle. A formal trace is short and stands for a whole family of failures. If it shows an illegal input, you add an assumption and re-solve. The tool then returns another trace or proves the case is gone, which new random seeds can never tell you.
Self-Check
Tick each key point you covered in your answer.
-
Scale ItTriaging Forty Formal FailuresL3 Senior
Your team brings up formal on a new block and reports forty failures in one morning. How do you triage them?
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
Expect most early failures to be environment problems, not RTL bugs. Bucket them by cause from step 0 and the solver-chosen inputs, fix reset and missing assumptions first, and rerun; many failures collapse together. Each assumption added is written from a spec row, reviewed, and paired with a cover. Only the failures that survive go to the designer as bugs.
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
"Formal found a failure, so the RTL has a bug."
This controller already has its fix, yet it fails at step 1. With no reset assumption and no initial values, the solver starts it in a state reset never produces. Declaring initial values makes it pass.
Run It
The fixed handshake controller from lesson F1.4, with no reset assumption and no initial values.
module hs_ctrl(input clk, rst, req, abort, output reg ack);
reg pending;
reg pending_d;
reg [1:0] busy_cnt;
always @(posedge clk) begin
if (rst) begin pending<=0; pending_d<=0; busy_cnt<=0; ack<=0; end
else begin
pending_d <= pending;
if (abort) pending <= 0;
else if (req) pending <= 1;
else if (busy_cnt == 2'd3) pending <= 0;
busy_cnt <= pending ? busy_cnt + 2'd1 : 2'd0;
ack <= pending && busy_cnt == 2'd3;
end
end
reg pending_q;
always @(posedge clk) begin
pending_q <= pending;
if (!rst && ack) assert(pending_q);
end
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 1
See the Fix
module hs_ctrl(input clk, rst, req, abort, output reg ack=0);
reg pending=0;
reg pending_d=0;
reg [1:0] busy_cnt=0;
always @(posedge clk) begin
if (rst) begin pending<=0; pending_d<=0; busy_cnt<=0; ack<=0; end
else begin
pending_d <= pending;
if (abort) pending <= 0;
else if (req) pending <= 1;
else if (busy_cnt == 2'd3) pending <= 0;
busy_cnt <= pending ? busy_cnt + 2'd1 : 2'd0;
ack <= pending && busy_cnt == 2'd3;
end
end
reg pending_q=0;
always @(posedge clk) begin
pending_q <= pending;
if (!rst && ack) assert(pending_q);
end
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
Misconception
Changes the RTL so that an impossible input sequence passes.
If the trace drives inputs no legal neighbour sends, the design is fine and the bench is under-constrained. The right fix is an assumption written from the spec.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 4 "Creating assumptions"; ch. 5 "Wiggling the design"
Delivery
Starts at step 0 and reads every signal forward.
Work back from the failure instead. The failing assertion's cone says which signals matter, and the first wrong value is usually a few steps earlier.