← Formal Verification Interviews
Interview Question · Design
Proving a Late Fix Changed Only the Bug
The Question
The interviewer asks
Two weeks before tape-out a designer fixes a WRAP-burst address bug. How do you show the fix changed nothing else?
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
Build a miter of the old and new RTL and check conditional equivalence. Outputs must match whenever the bug's condition is false. Inside that condition, the new design must meet the spec. Write the condition from the bug report, never from the diff, or a wrong fix defines its own condition. A counterexample on inputs the spec forbids means a missing assumption, not a bad fix.
Read the diagram as text
- Shared inputs: start, len, size, burst, n
- axi_addr, FIX 0: WRAP addressed like INCR
- axi_addr, the fix: WRAP returns to its window
- burst != WRAP: addr_new == addr_old: the fix changed nothing else
- burst == WRAP: inside the window: the fix does what the spec says
- Shared inputs → axi_addr, FIX 0
- Shared inputs → axi_addr, the fix
- axi_addr, FIX 0 → burst != WRAP: addr_new == addr_old
- axi_addr, the fix → burst != WRAP: addr_new == addr_old
- axi_addr, the fix → burst == WRAP: inside the window
Both are assertions on one bench. A fix that passes both changed exactly the behaviour it meant to.
Read the diagram as text
- burst == WRAP: allowed to differ; must stay in the window
- FIXED and INCR: must agree with the old design
- The bad fix's point: INCR at 0x66FFFC39, beat 1
- A test suite: a handful of chosen points
- The bad fix's point → FIXED and INCR: lies in
The bad fix moved a point in the "must agree" region. No WRAP test can find it.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Senior)
A good senior answer uses conditional equivalence, with the condition taken from the bug report. It adds spec assumptions only when counterexamples show illegal inputs.
What Interviewers Listen For (Staff)
A good staff answer weighs a formal ECO check against a regression rerun for schedule risk. It makes the proof part of ECO sign-off, with the condition reviewed by someone other than the fixer.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItBreak ItCompareScale It
- Proving a Late Fix Changed Only the Bug
-
WhyThe Condition Is a SpecificationL3 Senior
Why is writing the condition of a conditional equivalence check the same job as writing formal assumptions?
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
Both say where the check applies. A condition that is too wide hides real differences, exactly as an over-constraining assumption hides bugs. So it needs the same discipline. It needs a written source in the bug report or the spec. It also needs a review by someone who did not write the fix.
Self-Check
Tick each key point you covered in your answer.
-
Break ItA Condition That Excludes Too MuchL3 Senior
Break it: the fix touched one opcode, but the condition excludes a whole opcode group. What can escape?
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
Inside the excluded region the old and new designs may differ freely, and the check says nothing. So a second, accidental change to another opcode in that group passes. Write the condition from the bug report, so it covers only the failing case. Then check the new design inside it against the spec.
Self-Check
Tick each key point you covered in your answer.
Misconception
"A wider condition is safer, because the check passes sooner."
Passing sooner is the danger. Every input inside the condition is no longer compared with the old design.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 8 "Conditional equivalence"
-
CompareA Miter vs a Regression Rerun for an ECOL3 Senior
Compare a conditional-equivalence miter with a full regression rerun as the check for a late fix.
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 regression samples the input space at the points its tests reach, and it takes hours or days. The miter covers every input in the region where the old and new designs must agree. For a block-level fix, it usually takes minutes. The regression still matters for what the miter does not state. That is the behaviour inside the bug condition and the system around the block.
Self-Check
Tick each key point you covered in your answer.
-
What IfAn ECO Counterexample on an Illegal BurstL2 Mid-LevelL3 Senior
With the correct fix, the check still fails, on a WRAP burst of length 3. The miter's environment is below, with the WRAP-length line still missing. What do you do?
systemverilog assume(size <= 3'd2); // a 32-bit bus assume(burst != 2'd3); // reserved encoding assume(n <= len); // a beat of this burst if (burst == WRAP) assume((start & ((32'd1 << size) - 32'd1)) == 32'd0); if (burst != WRAP) assert(addr_new == addr_old);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
AXI allows WRAP bursts of only 2, 4, 8 or 16 transfers, so length 3 cannot occur; add that rule as an assumption, citing the spec. Add only what a counterexample demands: in the lesson the alignment assumption turned out unnecessary, because the check passes without it.
module axi_addr #(parameter FIX = 3)(input [31:0] start, input [3:0] len, input [2:0] size, input [1:0] burst, input [3:0] n, output [31:0] addr); localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2; wire [31:0] nb = 32'd1 << size; // bytes per transfer wire [31:0] aligned = start & ~(nb - 32'd1); // start aligned down to the transfer size wire [31:0] window = ({28'd0, len} + 32'd1) << size; // bytes in the whole burst wire [31:0] boundary = start & ~(window - 32'd1); // the wrap boundary (window is a power of two for WRAP) wire [31:0] a = aligned + ({28'd0, n} << size); wire wraps = FIX == 0 ? 1'b0 : FIX == 2 ? burst != FIXED : burst == WRAP; wire past_end = FIX == 1 ? a >= boundary + window : a - boundary >= window; assign addr = (burst == FIXED || n == 4'd0) ? start : (wraps && past_end) ? a - window : a; endmodule module eco_top(input clk, input [31:0] start, input [3:0] len, input [2:0] size, input [1:0] burst, input [3:0] n); localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2; wire [31:0] addr_old, addr_new; axi_addr #(.FIX(0)) old_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_old)); axi_addr #(.FIX(3)) new_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_new)); `ifdef FORMAL // modelling code: the WRAP window as the spec defines it, in 33 bits so the top of memory cannot overflow wire [32:0] f_window = ({29'd0, len} + 33'd1) << size; wire [32:0] f_boundary = ({1'b0, start} / f_window) * f_window; always @(posedge clk) begin assume(size <= 3'd2); // a 32-bit bus assume(burst != 2'd3); // reserved encoding assume(n <= len); // a beat of this burst if (burst == WRAP) assume((start & ((32'd1 << size) - 32'd1)) == 32'd0); if (burst != WRAP) assert(addr_new == addr_old); if (burst == WRAP && n != 4'd0) assert({1'b0, addr_new} >= f_boundary && {1'b0, addr_new} < f_boundary + f_window); end `endif endmodulePrints:
prove, depth 2 (smtbmc yices): FAIL at step 1Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F6.4.1: Constrain the Scope of a WRAP FixSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
Scale ItFormal ECO Checks in the Tape-Out FlowL4 Staff
How would you make formal ECO checks a standard step in a chip's tape-out flow?
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 late RTL change carries a miter against the last signed-off RTL. Its condition comes from its bug report, and a second engineer reviews it. The block's formal regression and RTL-to-netlist LEC rerun on the new netlist. The ECO is closed only when all three are clean and the condition is attached to the change record.
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
"The fix touches only the wrap logic, so it is obviously safe."
This "fix" also wraps INCR bursts. The check that non-WRAP addresses are unchanged fails at step 1; the correct fix passes the same check.
Run It
Old and new AXI address generators in one miter. The new one applies wrapping to every non-FIXED burst.
module axi_addr #(parameter FIX = 3)(input [31:0] start, input [3:0] len,
input [2:0] size, input [1:0] burst, input [3:0] n, output [31:0] addr);
localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
wire [31:0] nb = 32'd1 << size; // bytes per transfer
wire [31:0] aligned = start & ~(nb - 32'd1); // start aligned down to the transfer size
wire [31:0] window = ({28'd0, len} + 32'd1) << size; // bytes in the whole burst
wire [31:0] boundary = start & ~(window - 32'd1); // the wrap boundary (window is a power of two for WRAP)
wire [31:0] a = aligned + ({28'd0, n} << size);
wire wraps = FIX == 0 ? 1'b0 : FIX == 2 ? burst != FIXED : burst == WRAP;
wire past_end = FIX == 1 ? a >= boundary + window : a - boundary >= window;
assign addr = (burst == FIXED || n == 4'd0) ? start : (wraps && past_end) ? a - window : a;
endmodule
module eco_top(input clk, input [31:0] start, input [3:0] len, input [2:0] size, input [1:0] burst, input [3:0] n);
localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
wire [31:0] addr_old, addr_new;
axi_addr #(.FIX(0)) old_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_old));
axi_addr #(.FIX(2)) new_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_new));
`ifdef FORMAL
// modelling code: the WRAP window as the spec defines it, in 33 bits so the top of memory cannot overflow
wire [32:0] f_window = ({29'd0, len} + 33'd1) << size;
wire [32:0] f_boundary = ({1'b0, start} / f_window) * f_window;
always @(posedge clk) begin
assume(size <= 3'd2); // a 32-bit bus
assume(burst != 2'd3); // reserved encoding
assume(n <= len); // a beat of this burst
if (burst == WRAP) assume(len == 4'd1 || len == 4'd3 || len == 4'd7 || len == 4'd15);
if (burst == WRAP) assume((start & ((32'd1 << size) - 32'd1)) == 32'd0);
if (burst != WRAP) assert(addr_new == addr_old);
if (burst == WRAP && n != 4'd0) assert({1'b0, addr_new} >= f_boundary && {1'b0, addr_new} < f_boundary + f_window);
end
`endif
endmodule
Prints: prove, depth 2 (smtbmc yices): FAIL at step 1
See the Fix
module axi_addr #(parameter FIX = 3)(input [31:0] start, input [3:0] len,
input [2:0] size, input [1:0] burst, input [3:0] n, output [31:0] addr);
localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
wire [31:0] nb = 32'd1 << size; // bytes per transfer
wire [31:0] aligned = start & ~(nb - 32'd1); // start aligned down to the transfer size
wire [31:0] window = ({28'd0, len} + 32'd1) << size; // bytes in the whole burst
wire [31:0] boundary = start & ~(window - 32'd1); // the wrap boundary (window is a power of two for WRAP)
wire [31:0] a = aligned + ({28'd0, n} << size);
wire wraps = FIX == 0 ? 1'b0 : FIX == 2 ? burst != FIXED : burst == WRAP;
wire past_end = FIX == 1 ? a >= boundary + window : a - boundary >= window;
assign addr = (burst == FIXED || n == 4'd0) ? start : (wraps && past_end) ? a - window : a;
endmodule
module eco_top(input clk, input [31:0] start, input [3:0] len, input [2:0] size, input [1:0] burst, input [3:0] n);
localparam FIXED = 2'd0, INCR = 2'd1, WRAP = 2'd2;
wire [31:0] addr_old, addr_new;
axi_addr #(.FIX(0)) old_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_old));
axi_addr #(.FIX(3)) new_(.start(start), .len(len), .size(size), .burst(burst), .n(n), .addr(addr_new));
`ifdef FORMAL
// modelling code: the WRAP window as the spec defines it, in 33 bits so the top of memory cannot overflow
wire [32:0] f_window = ({29'd0, len} + 33'd1) << size;
wire [32:0] f_boundary = ({1'b0, start} / f_window) * f_window;
always @(posedge clk) begin
assume(size <= 3'd2); // a 32-bit bus
assume(burst != 2'd3); // reserved encoding
assume(n <= len); // a beat of this burst
if (burst == WRAP) assume(len == 4'd1 || len == 4'd3 || len == 4'd7 || len == 4'd15);
if (burst == WRAP) assume((start & ((32'd1 << size) - 32'd1)) == 32'd0);
if (burst != WRAP) assert(addr_new == addr_old);
if (burst == WRAP && n != 4'd0) assert({1'b0, addr_new} >= f_boundary && {1'b0, addr_new} < f_boundary + f_window);
end
`endif
endmodule
Prints: prove, depth 2 (smtbmc yices): PASS
Misconception
"Write the condition from the lines the diff changed."
Then every behaviour the fix changed sits inside the condition by definition and is never compared. The condition must describe the bug, from the report.
Source Seligman, Schubert and Kiran Kumar, Formal Verification (2nd ed.) ch. 8 "Conditional equivalence"
Half-Truth
"Rerunning the regression is enough for a one-line fix."
The regression samples a few points. The miter checks every input in the region where the two designs must agree.