← Formal Verification Interviews
Interview Question · Debug
False Failures from Free Inputs
The Question
The interviewer asks
A read slave that passes all its simulation tests fails formal at step 5. In the trace, the master changes araddr while arvalid is still waiting for arready. What is going on?
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
The inputs are free, so the solver drove a sequence no legal master sends: it changed the address during a stall. The failure is false; the bench is under-constrained. Add one assumption from the spec row and cite the row. It says arvalid stays high and the address stays stable until the handshake. Then cover the stall and the handshake so the assumption did not go too far.
Read the diagram as text
- 1. Is step 0 a reset state?: no: fix the reset assumption (F1.6)
- 2. Is every shaded input legal?: check each value against the spec row, step by step
- 3. Does the check say what the spec says?: implication, delay, the signal it reads
- 4. RTL bug: only now is the design wrong
- Add one assumption: on inputs, with the spec row in its comment
- Fix the property: the design may be right
- 1. Is step 0 a reset state? → 2. Is every shaded input legal?: yes
- 2. Is every shaded input legal? → 3. Does the check say what the spec says?: yes
- 3. Does the check say what the spec says? → 4. RTL bug: yes
- 2. Is every shaded input legal? → Add one assumption: no
- 3. Does the check say what the spec says? → Fix the property: no
Ask the questions in order and stop at the first "no". Run A stops at question 2: an input broke the protocol.
The measured trace from lesson F3.3. Shaded rows are inputs the solver chose; follow araddr while arvalid waits.
Measured with smtbmc yices at depth 20. The addresses are the solver's choice. The response at step 4 carries the captured FE plus one; the rule expects 7E plus one.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Junior)
A good junior answer recognises a false failure caused by an illegal input sequence. It writes the missing assumption from the protocol rule.
What Interviewers Listen For (Mid-Level)
A good mid-level answer triages in order: reset state, each input against the spec, the property, and only then the RTL. After the fix it covers the stall, the handshake and payload extremes.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItBreak ItCompare
- False Failures from Free Inputs
-
WhyWhy Start with Few AssumptionsL1 JuniorL2 Mid-Level
Why start a formal bench with few assumptions instead of writing them all from the spec on day 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
A long list written up front is likely to include rules stronger than the real environment, and nothing tells you which. Starting loose means you add each assumption in answer to a trace that showed an illegal input. So every assumption has a reason and a spec row. The false failures are cheap; a silent over-constraint is not.
Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F3.3.1: Four Traces, Four CausesSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
CompareUnder-Constraint vs Over-ConstraintL1 JuniorL2 Mid-Level
Compare under-constraint and over-constraint. Which one is more dangerous?
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
Under-constraint gives false failures: they cost debug time, but every one is visible in a trace. Over-constraint gives false passes, which look exactly like real ones. Over-constraint is the dangerous one, and covers under the full assumption set are the only routine defence against it.
Self-Check
Tick each key point you covered in your answer.
-
Break ItAn Assumption That Went Too FarL2 Mid-Level
To silence the failure, someone adds the assumption below. The assertion now passes. What broke?
systemverilog reg [7:0] araddr_q = 0; // last cycle's araddr always @(posedge clk) araddr_q <= araddr; always @(posedge clk) assume(araddr == araddr_q);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 address is now stuck at its starting value, so most legal reads never happen. The pass says nothing about other addresses. A cover of a handshake at address
8'hFFcomes back unreached, which shows the assumption removed legal traffic.module rd_slave_sp(input clk, rst, arvalid, input [7:0] araddr, input rready, output arready, output reg rvalid=0, output reg [7:0] rdata=0); reg [7:0] addr_cap=0; // the speculative copy reg waited=0; // arvalid was high last cycle without a handshake assign arready = !rvalid; always @(posedge clk) if (rst) begin rvalid <= 0; waited <= 0; end else begin if (arvalid && !waited) addr_cap <= araddr; // capture in the first arvalid cycle waited <= arvalid && !arready; if (rvalid && rready) rvalid <= 0; else if (arvalid && arready) begin rvalid <= 1; rdata <= (waited ? addr_cap : araddr) + 8'd1; end end `ifdef FORMAL always @(posedge clk) begin if ($initstate) begin assume(rst); end else begin assume(!rst); end end reg [7:0] araddr_q=0; // last cycle's araddr, the registered form of $past(araddr) always @(posedge clk) araddr_q <= araddr; always @(posedge clk) assume(araddr == araddr_q); `endif endmodulePrints:
cover, depth 20 (smtbmc yices): FAIL at step 3, cover unreachedSelf-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F3.3.2: One Promise for Speculative CaptureSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfThe Assumption That Should Have Been WrittenL2 Mid-Level
What should the assumption have said instead, and how do you show it is not too strong as well?
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
Write the spec rule: while
arvalidwaits forarready, the address holds. In this bench that isarvalid && !arready |=> araddr == araddr_q. Between transfers the address is free again. Then rerun the covers: the stall, the handshake and the handshake at8'hFFmust all be reached.Self-Check
Tick each key point you covered in your answer.
Half-Truth
"Assume the address is stable whenever
arvalidis high."That also holds it across back-to-back transfers, where
arvalidnever drops. The next address could never change, so legal traffic disappears again.
What People Get Wrong
Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.
Misconception
"Formal shows the slave mishandles a changing address, so fix the RTL."
AXI requires a source to hold VALID and its payload stable until the handshake. With that one assumption the same RTL passes to depth 20.
Run It
The speculative read slave from lesson F3.3, with no assumption on the master.
module rd_slave_sp(input clk, rst, arvalid, input [7:0] araddr, input rready,
output arready, output reg rvalid=0, output reg [7:0] rdata=0);
reg [7:0] addr_cap=0; // the speculative copy
reg waited=0; // arvalid was high last cycle without a handshake
assign arready = !rvalid;
always @(posedge clk)
if (rst) begin rvalid <= 0; waited <= 0; end
else begin
if (arvalid && !waited) addr_cap <= araddr; // capture in the first arvalid cycle
waited <= arvalid && !arready;
if (rvalid && rready) rvalid <= 0;
else if (arvalid && arready) begin
rvalid <= 1;
rdata <= (waited ? addr_cap : araddr) + 8'd1;
end
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg [7:0] araddr_q=0; // last cycle's araddr, the registered form of $past(araddr)
always @(posedge clk) araddr_q <= araddr;
reg ar_hs_q=0, r_stall_q=0;
reg [7:0] rdata_q=0;
always @(posedge clk) begin
ar_hs_q <= !rst && arvalid && arready;
r_stall_q <= !rst && rvalid && !rready;
rdata_q <= rdata;
if (!rst && ar_hs_q) assert(rvalid && rdata == araddr_q + 8'd1);
if (!rst && r_stall_q) assert(rvalid && rdata == rdata_q);
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 5
See the Fix
module rd_slave_sp(input clk, rst, arvalid, input [7:0] araddr, input rready,
output arready, output reg rvalid=0, output reg [7:0] rdata=0);
reg [7:0] addr_cap=0; // the speculative copy
reg waited=0; // arvalid was high last cycle without a handshake
assign arready = !rvalid;
always @(posedge clk)
if (rst) begin rvalid <= 0; waited <= 0; end
else begin
if (arvalid && !waited) addr_cap <= araddr; // capture in the first arvalid cycle
waited <= arvalid && !arready;
if (rvalid && rready) rvalid <= 0;
else if (arvalid && arready) begin
rvalid <= 1;
rdata <= (waited ? addr_cap : araddr) + 8'd1;
end
end
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg [7:0] araddr_q=0; // last cycle's araddr, the registered form of $past(araddr)
always @(posedge clk) araddr_q <= araddr;
reg ar_stall_q=0;
always @(posedge clk) begin
ar_stall_q <= !rst && arvalid && !arready;
if (!rst && ar_stall_q) assume(arvalid && araddr == araddr_q);
end
reg ar_hs_q=0, r_stall_q=0;
reg [7:0] rdata_q=0;
always @(posedge clk) begin
ar_hs_q <= !rst && arvalid && arready;
r_stall_q <= !rst && rvalid && !rready;
rdata_q <= rdata;
if (!rst && ar_hs_q) assert(rvalid && rdata == araddr_q + 8'd1);
if (!rst && r_stall_q) assert(rvalid && rdata == rdata_q);
end
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
Misconception
"Add assumptions until the failures stop."
Each assumption must come from a spec rule. Assuming until it passes is how over-constraint happens, and the last assumption added often hides the real bug.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 4 "Creating assumptions"; ch. 9 "Vacuity issues"