← Formal Verification Interviews
Interview Question · Debug
Simulation Passes, Formal Fails on an Unreset Flop
The Question
The interviewer asks
A mode register has no reset, because firmware writes it before start. Simulation passes, but formal fails at step 3. Who is right?
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
Both, about different things. In formal the unreset mode is free at step 0. So the solver picked the value that enables the block before firmware wrote anything. Simulation started mode at one value per run, and a default run never hit the bad one. Either reset the flop, or write the firmware promise as an initial-state assumption and put it on the sign-off list.
Read the diagram as text
- mode[3:0], no reset: four-state sim: X. Two-state sim: 0. Formal: any value, chosen per run
- mode == 4'd3: four-state: X. Two-state: 0. Formal: 1 if the solver chose 3
- en = armed && (mode == 3): four-state: X once armed
- if (en) in a consumer: four-state: X counts as false, the else branch runs
- gate-level simulation: the X spreads through the netlist: pessimism
- silicon: the flop powers up 0 or 1 per bit; sometimes 3
- mode[3:0], no reset → mode == 4'd3
- mode == 4'd3 → en = armed && (mode == 3)
- en = armed && (mode == 3) → if (en) in a consumer: optimism
- en = armed && (mode == 3) → gate-level simulation
- mode[3:0], no reset → silicon
Neither simulation says what the hardware does. Formal has no X: it treats the unknown as a value it may pick, and picks the one that breaks the rule.
The measured counterexample from lesson F5.5: mode is 3 at step 0, start arms the block, and en rises with no firmware write ever seen.
Measured with smtbmc yices at depth 20. The flop has no reset, so its first value is the solver's choice: 3. Sampled at step 2, reported at 3.
Self-Check
Tick each key point you covered in your answer.
What Interviewers Listen For (Junior)
A good junior answer explains that formal treats a flop without a reset as any value. One simulation run sees just one value.
What Interviewers Listen For (Senior)
A good senior answer puts each initial-state assumption on the sign-off list with an owner. It makes X-propagation on outputs a sign-off item. It weighs a reset against the firmware rule for area and power.
Cross-Questions
Where the interviewer goes next. Open a node to practise that follow-up.
WhyWhat IfProve ItBreak ItCompare
- Simulation Passes, Formal Fails on an Unreset Flop
-
WhyWhy an Unreset Flop Is a Free ValueL1 Junior
Why does a formal tool treat an unreset flop as any value, instead of X as simulation does?
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
Formal models are two-valued, and silicon powers up to some real 0 or 1 in each flop. Leaving the start value free lets the solver try every possibility in one run. Four-state simulation instead carries an X that
ifstatements can silently resolve, so it may never show the bad value.Self-Check
Tick each key point you covered in your answer.
-
CompareX-Optimism, X-Pessimism and Free ValuesL1 JuniorL2 Mid-Level
Compare X-optimism, X-pessimism and the way formal handles an unknown start value.
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
X-optimism is RTL simulation resolving an unknown too kindly, so a bug hides. For example, an
ifon X takes the else branch. X-pessimism is gate-level simulation spreading X further than real hardware would, which floods the run with false unknowns. Formal is two-valued and leaves the value free, so it checks both 0 and 1 and reports the one that breaks a property.Self-Check
Tick each key point you covered in your answer.
-
Break ItWhy Random Initial Values Are Not EnoughL1 JuniorL2 Mid-Level
A colleague says random initial values in simulation are as good as formal for unreset flops. Break that claim.
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 random initial value is one draw per run. If only a few start values break the rule, most seeds pass. Formal treats the start value as free, so one run checks every value. The solver then picks a value that breaks the property, if one exists.
Self-Check
Tick each key point you covered in your answer.
Half-Truth
"Run enough seeds and random initial values will find it."
Each seed samples one start state. A 32-bit register has about four billion of them, so a rare bad value is unlikely to be drawn.
-
Prove ItSolve F5.5.1: Reset the Free Mode BitSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
-
What IfAn Explicit X in FormalL2 Mid-Level
What does a formal tool do with the output below, which the RTL assigns as
1'bx?systemverilog assign dbg = 1'bx; always @(posedge clk) if (!rst) assert(!dbg);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
In this flow an explicit
xbecomes a free value the solver may choose on every cycle. An assertion that the debug output stays low therefore fails, here at step 2. That is useful. A strayxdefault in a case statement shows up as a real failure, not a silent simulation quirk.module xcmp(input clk, rst, fw_wr, input [3:0] fw_data, input start, output en, output dbg); reg [3:0] mode; reg armed=0; always @(posedge clk) begin if (rst) mode <= 4'd0; else if (fw_wr) mode <= fw_data; if (rst) armed <= 0; else if (start) armed <= 1; end assign en = armed && mode == 4'd3; assign dbg = 1'bx; `ifdef FORMAL always @(posedge clk) begin if ($initstate) begin assume(rst); end else begin assume(!rst); end end reg fw_seen=0; // firmware has written mode at least once (a write during reset counts too) always @(posedge clk) if (fw_wr) fw_seen <= 1; always @(posedge clk) if (!rst && en) assert(fw_seen); always @(posedge clk) if (!rst) assert(!dbg); `endif endmodulePrints:
bmc, depth 20 (smtbmc yices): FAIL at step 2Self-Check
Tick each key point you covered in your answer.
-
Prove ItSolve F5.5.2: Keep an Unknown from Enabling the BlockSimulator-graded
Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
What People Get Wrong
Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.
Misconception
"Simulation with random initial values passed, so the flop is fine."
A random start value is one draw per run. In the lesson 11 of 100 seeds found the early enable and the first three did not; formal checks every value in one run.
Run It
The mode register from lesson F5.5, with no reset; the property says the block is enabled only after firmware wrote mode.
module xcmp(input clk, rst, fw_wr, input [3:0] fw_data, input start, output en);
reg [3:0] mode; // no reset: firmware writes it before start
reg armed=0;
always @(posedge clk) begin
if (1'b0) mode <= 4'd0; // FIX_RESET puts rst here
else if (fw_wr) mode <= fw_data;
if (rst) armed <= 0; else if (start) armed <= 1;
end
assign en = armed && mode == 4'd3;
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg fw_seen=0; // firmware has written mode at least once (a write during reset counts too)
always @(posedge clk) if (fw_wr) fw_seen <= 1;
always @(posedge clk) if (!rst && en) assert(fw_seen);
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 3
See the Fix
module xcmp(input clk, rst, fw_wr, input [3:0] fw_data, input start, output en);
reg [3:0] mode;
reg armed=0;
always @(posedge clk) begin
if (rst) mode <= 4'd0;
else if (fw_wr) mode <= fw_data;
if (rst) armed <= 0; else if (start) armed <= 1;
end
assign en = armed && mode == 4'd3;
`ifdef FORMAL
always @(posedge clk) begin
if ($initstate) begin assume(rst); end else begin assume(!rst); end
end
reg fw_seen=0; // firmware has written mode at least once (a write during reset counts too)
always @(posedge clk) if (fw_wr) fw_seen <= 1;
always @(posedge clk) if (!rst && en) assert(fw_seen);
`endif
endmodule
Prints: bmc, depth 20 (smtbmc yices): PASS
Half-Truth
"Four-state simulation would show the X and catch it."
An if on X takes the else branch, so RTL simulation can hide the unknown. Gate-level simulation, by contrast, can flood the netlist with X. Neither says what silicon does.
Source IEEE 1800-2017 §12.4; Sutherland, RTL Modeling with SystemVerilog, §5.1.2