Interview Question · Debug

Reset and the Initial State in Formal

L0 FresherL1 Juniorresetformal basics

The interviewer asks

Your first formal run on a decade counter fails at step 1 with count = 12. The RTL has a synchronous reset. What went wrong?

Reveal the Model Answer

Nothing told the tool how the design starts, so every state, including count = 12, was a legal initial state. Assume reset in the first step, for example if ($initstate) assume(rst), or declare initial values. A flop with no reset or initial value stays a free choice at step 0. The solver picks whichever value breaks the property.

Where reachability starts

With the reset assumed, the initial set is the single state count = 0 and the rings stay inside 0 to 9. With no reset assumption every state is initial, so count = 12 is reachable in zero steps.

Under the reset assumption, count stays in 0 to 9: 12 and 15 lie outside every ring and the check passes to depth 20. With no reset assumption the initial cloud is the whole map, 12 is an initial state, and the check fails in step 0.

Read the states and transitions

0: initial, depth 0.
1: reachable, depth 1.
2: reachable, depth 2.
9: reachable, depth 9.
12: bad, depth 0.
15: unreachable, depth 0.
0 → 1.
1 → 2.
9 → 0.
12 → 15.

Illustration. A drawing of the two initial sets with the measured values. The real counter has 16 states; only the ones the page names are drawn.

The measured counterexample: rst is never asserted, so step 0 already holds count = 12, a value reset would never produce.

No reset assumption: the counter starts wherever the solver likes

Measured: FAIL at reported step 1, 600 ms. The value 12 is the solver's choice; another solver may pick any value from 10 to 15.

The decade counter from lesson F1.6 with no reset assumption.

module ctr10(input clk, rst, en, output reg [3:0] count);
  wire [3:0] step = 4'd1;
  always @(posedge clk) begin
    if (rst) count <= 4'd0;
    else if (en) count <= (count == 4'd9) ? 4'd0 : count + step;
  end
  always @(posedge clk) if (!rst) begin
    assert(count <= 4'd9);
  end
endmodule

Prints: bmc, depth 20 (smtbmc yices): FAIL at step 1

Self-Check

Tick each key point you covered in your answer.

Key point 1 Nothing told the tool how the design starts, so every state, including count = 12, was a legal initial state. Key point 2 Assume reset in the first step, for example if ($initstate) assume(rst), or declare initial values. Key point 3 A flop with no reset or initial value stays a free choice at step 0. Key point 4 The solver picks whichever value breaks the property.

What Interviewers Listen For (Fresher)

A good fresher answer says formal needs a reset or an initial state. It knows that a flop without a reset can start at any value.

Cross-Questions

Where the interviewer goes next. Open a node to practise that follow-up.

WhyWhat IfProve ItBreak ItCompare

Reset and the Initial State in Formal
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?

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 if statements can silently resolve, so it may never show the bad value.

Self-Check
Tick each key point you covered in your answer.
Key point 1 Formal models are two-valued, and silicon powers up to some real 0 or 1 in each flop. Key point 2 Leaving the start value free lets the solver try every possibility in one run. Key point 3 Four-state simulation instead carries an X that if statements can silently resolve, so it may never show the bad value.
- Lesson F1.6Reset, the Initial State and $initstate
- Lesson F5.5X-Propagation
CompareThree Ways to Model ResetL1 JuniorL2 Mid-Level
Compare assuming reset in the first step, declaring initial values and holding reset with a small counter.

Reveal the Model Answer

All three make the decade counter pass at depth 20 in the lesson. Assuming reset at $initstate checks the real reset logic and is closest to silicon. Declared initial values skip the reset path, so a bug in it can hide. A reset counter models a multi-cycle reset sequence at the cost of a little depth.

Self-Check
Tick each key point you covered in your answer.
Key point 1 All three make the decade counter pass at depth 20 in the lesson. Key point 2 Assuming reset at $initstate checks the real reset logic and is closest to silicon. Key point 3 Declared initial values skip the reset path, so a bug in it can hide. Key point 4 A reset counter models a multi-cycle reset sequence at the cost of a little depth.
- Lesson F1.6Reset, the Initial State and $initstate
Prove ItSolve F1.6.1: Reset the Mode as Well as the CountSimulator-graded

Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
Open Problem F1.6.1
What IfSimulation Passes, Formal Fails on an Unreset FlopL1 JuniorL2 Mid-Level
A mode register has no reset, because firmware writes it before start. Simulation passes, but formal fails at step 3. Who is right?
2:30

You have two and a half minutes. Speak or type, then press Get Feedback under your answer. No credits needed.

Your level

Speech-to-text runs in your browser. Chrome and Edge may send audio to their own speech service.
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.

One Unreset Flop, Three ReadingsThe same path read by four-state simulation, a two-state simulator and formal. Arrows mean "feeds".

data: where the transaction goes

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.

mode starts at 3, and no firmware write ever came
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.
Key point 1 Both, about different things. Key point 2 In formal the unreset mode is free at step 0. Key point 3 So the solver picked the value that enables the block before firmware wrote anything. Key point 4 Simulation started mode at one value per run, and a default run never hit the bad one. Key point 5 Either reset the flop, or write the firmware promise as an initial-state assumption and put it on the sign-off list.

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.
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
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?

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 if statements can silently resolve, so it may never show the bad value.

Self-Check
Tick each key point you covered in your answer.
Key point 1 Formal models are two-valued, and silicon powers up to some real 0 or 1 in each flop. Key point 2 Leaving the start value free lets the solver try every possibility in one run. Key point 3 Four-state simulation instead carries an X that if statements can silently resolve, so it may never show the bad value.
- Lesson F1.6Reset, the Initial State and $initstate
- Lesson F5.5X-Propagation
CompareX-Optimism, X-Pessimism and Free ValuesL1 JuniorL2 Mid-Level
Compare X-optimism, X-pessimism and the way formal handles an unknown start value.

Reveal the Model Answer

X-optimism is RTL simulation resolving an unknown too kindly, so a bug hides. For example, an if on 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.
Key point 1 X-optimism is RTL simulation resolving an unknown too kindly, so a bug hides. Key point 2 For example, an if on X takes the else branch. Key point 3 X-pessimism is gate-level simulation spreading X further than real hardware would, which floods the run with false unknowns. Key point 4 Formal is two-valued and leaves the value free, so it checks both 0 and 1 and reports the one that breaks a property.
- Lesson F5.5X-Propagation
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.

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.
Key point 1 A random initial value is one draw per run. Key point 2 If only a few start values break the rule, most seeds pass. Key point 3 Formal treats the start value as free, so one run checks every value. Key point 4 The solver then picks a value that breaks the property, if one exists.

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.
- Lesson F5.5X-Propagation
- Problem F5.5.1Reset the Free Mode Bit
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.
Open Problem F5.5.1
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:30

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.
Reveal the Model Answer

In this flow an explicit x becomes 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 stray x default 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 endmodule
Prints: bmc, depth 20 (smtbmc yices): FAIL at step 2

Self-Check
Tick each key point you covered in your answer.
Key point 1 In this flow an explicit x becomes a free value the solver may choose on every cycle. Key point 2 An assertion that the debug output stays low therefore fails, here at step 2. Key point 3 That is useful. Key point 4 A stray x default in a case statement shows up as a real failure, not a silent simulation quirk.
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.
Open Problem F5.5.2

What People Get Wrong

Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.

Misconception

"Flops start at zero, as in simulation."

In the formal model a flop with no reset or initial value is free in step 0. This counter fails at step 1 for exactly that reason, and passes once reset is assumed in the first step.

Run It

No reset assumption: the solver chooses the starting count.

module ctr10(input clk, rst, en, output reg [3:0] count);
  wire [3:0] step = 4'd1;
  always @(posedge clk) begin
    if (rst) count <= 4'd0;
    else if (en) count <= (count == 4'd9) ? 4'd0 : count + step;
  end
  always @(posedge clk) if (!rst) begin
    assert(count <= 4'd9);
  end
endmodule

Prints: bmc, depth 20 (smtbmc yices): FAIL at step 1

See the Fix

module ctr10(input clk, rst, en, output reg [3:0] count);
  wire [3:0] step = 4'd1;
  always @(posedge clk) begin
    if (rst) count <= 4'd0;
    else if (en) count <= (count == 4'd9) ? 4'd0 : count + step;
  end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assert(count <= 4'd9);
  end
endmodule

Prints: bmc, depth 20 (smtbmc yices): PASS

Missed Corner

"Assume rst is always high and the counter is safe."

Holding reset for the whole run makes every assertion pass vacuously, because the counter never counts. The cover of count == 9 comes back unreached.

Run It

Reset assumed on every cycle, with a cover of the counter reaching 9.

module ctr10(input clk, rst, en, output reg [3:0] count);
  wire [3:0] step = 4'd1;
  always @(posedge clk) begin
    if (rst) count <= 4'd0;
    else if (en) count <= (count == 4'd9) ? 4'd0 : count + step;
  end
  always @(posedge clk) assume(rst);
  always @(posedge clk) if (!rst) begin
    assert(count <= 4'd9);
    cover(count == 4'd9);
  end
endmodule

Prints: cover, depth 20 (smtbmc yices): FAIL, cover unreached

See the Fix

module ctr10(input clk, rst, en, output reg [3:0] count);
  wire [3:0] step = 4'd1;
  always @(posedge clk) begin
    if (rst) count <= 4'd0;
    else if (en) count <= (count == 4'd9) ? 4'd0 : count + step;
  end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    assert(count <= 4'd9);
    cover(count == 4'd9);
  end
endmodule

Prints: cover, depth 20 (smtbmc yices): PASS at step 11, cover reached

Half-Truth

"A strap flop that firmware loads needs no reset."

It may be right for silicon, but in formal it is a free value. Write the firmware promise as an initial-state assumption and put it on the sign-off list, or add the reset.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.

Reset and the Initial State in Formal

Your Answer

Self-Check

What Interviewers Listen For (Fresher)

What Interviewers Listen For (Mid-Level)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What Interviewers Listen For (Junior)

What Interviewers Listen For (Senior)

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It

The Question

Your Answer

Self-Check

What Interviewers Listen For (Fresher)

What Interviewers Listen For (Mid-Level)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What Interviewers Listen For (Junior)

What Interviewers Listen For (Senior)

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It