Reset, the Initial State and $initstate

Tell the tool how the design starts: assume the reset in the first step, declare initial values or hold the reset, and treat every unreset flop as a free variable.

Lesson: F1.6
Time: 20 min
Runs on: SymbiYosys
Check: 4 questions

A modulo-10 counter failed its first formal run in step 0: count was 12. The designer said "that cannot happen, the counter resets to 0", but the bench had never told the tool that reset is asserted at the start. To a prover, a flop with no stated initial value can start anywhere. Later a mode strap with no reset at all, which the designer "knew" the boot code set first, turned the block's proofs into a coin toss.

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.

Where the Design Starts

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.

Reachability starts from the initial states. If nothing constrains them, every state is initial and the cloud is the whole map. Every state is then reachable in zero steps, and a property that is false in any state fails in step 0. A formal run must be told how the design starts. In simulation the reset sequence does that; in formal it is an assumption, and the tool holds you to it.

Three Ways to Say It

Way	Code	What the tool does	Measured
Assume `rst` in the first step	`if ($initstate) assume(rst); else assume(!rst);`	The RTL's own reset logic takes the design to its reset state at step 1.	BMC PASS to depth 20
Declare initial values	`reg [3:0] count = 0;`	Yosys's formal front end honours the initialiser as the initial state. `rst` stays free.	BMC PASS to depth 20
Hold the reset for n cycles	`assume(rst == (rst_cnt < 2));` with a small counter	For designs that need more than one reset cycle. `rst` is 1 at steps 0 and 1.	BMC PASS to depth 20
The wrong way: `assume(rst);` with no guard	`always @(posedge clk) assume(rst);`	Reset never releases. The assert passes and `cover(count == 9)` is unreached.	BMC PASS to depth 20; cover unreached within the depth

With the first way, cover(count == 9) is cover reached, reported step 11: the counter really runs. A cover beside every reset idiom catches the wrong one (F1.3).

$initstate is a Yosys formal function: 1 in the first step, 0 afterwards. The reset assumption on this site holds rst high in that step and low from then on, so the trace shows one reset step and the design free to run. Asynchronous resets need multiclock on or async2sync in the task; the F1 and F2 designs use synchronous reset, and F3.1 covers the asynchronous case with disable iff (A3.5 Reset and abort).

An Unreset Flop Is a Free Choice

An unreset strap flop: free in step 0, then held

Measured: FAIL at reported step 7, 642 ms. mode is shaded because its step-0 value is free; from step 1 the RTL holds it. count is also free at step 0 (12), but the assumed reset clears it at step 1.

Where the Fix for an Unreset Flop BelongsArrows mean "leads to". The trace shows the free value; the question is whether the chip can reset the flop or whether something outside the block sets it.

Read the diagram as text

Free value in step 0: mode = 1 in the trace
Can the chip reset it?: area, timing, the spec
Reset it in the RTL: the proof needs no assumption
Assume it under $initstate: the boot chain loads it
Sign-off assumption list: reviewed with the firmware team (F7.3)

Free value in step 0 → Can the chip reset it?
Can the chip reset it? → Reset it in the RTL: yes
Can the chip reset it? → Assume it under $initstate: no
Assume it under $initstate → Sign-off assumption list: write it down

Both fixes make the run pass. Only one of them changes the silicon, and only the other needs a reviewer.

Fix in the RTL

always @(posedge clk)
  if (rst) mode <= 1'b0;

Right when the chip really resets the strap. Changes the silicon.

Fix in the assumptions

always @(posedge clk)
  if ($initstate) assume(!mode);

Right when the boot chain really loads 0 first. Goes into the sign-off list (F7.3). Measured: BMC PASS to depth 20.

A flop with no reset and no initial value is a free choice in step 0 only; after that the RTL drives it. The tool picks the value that breaks the property. If firmware really writes it first, that is an assumption to write down and a fact to put in the sign-off's assumption list, where a reviewer can disagree. The free initial state returns in F2.4: an induction trace starts from any state, not only from reset.

Asked in Interviews

Question	Answer
Why does the trace start from a strange state?	The initial state was not constrained, or the trace is an induction trace (F2.4).
How do you model reset in formal?	Assume it in the initial step and let the RTL reset itself; or declare initial values; hold it as long as the design needs.
What about a flop that firmware initialises?	An assumption under $initstate, written down and reviewed at sign-off; or a reset in the RTL if the chip can afford it.

Try It

Concurrent SVA

assert property (@(posedge clk) disable iff (rst) count <= 4'd9);

The counter never passes 9, outside reset.

As this engine runs it, plus the reset assumption

always @(posedge clk) begin
  if ($initstate) assume(rst); else assume(!rst);
end
always @(posedge clk) if (!rst)
  assert(count <= 4'd9);

The assumption is formal-only code; disable iff becomes the !rst guard.

The whole task. The page leaves depth at the default, 20.

[options]
mode bmc
depth 20
[engines]
smtbmc yices
[script]
read_verilog -formal -sv design.sv
prep -top ctr10
[files]
design.sv

No reset
Run as it is: FAIL at reported step 1. Read step 0: count is 12 before anything happened.
Assume the reset
Add always @(posedge clk) if ($initstate) assume(rst); else assume(!rst); and run: BMC PASS to depth 20. Then try the other two ways instead: reg [3:0] count = 0; with no assumption, and the held-reset counter.
The strap
Add reg mode; always @(posedge clk) mode <= mode; and make step equal mode ? 4'd2 : 4'd1. Run: FAIL at reported step 7, with mode 1 at step 0 and count going 8 to 10.
Choose the fix
Either reset mode in the RTL or add if ($initstate) assume(!mode);. Both pass. Which belongs in the RTL and which in the sign-off assumption list?

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

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

Check Yourself

Predict the outputctr10, no reset assumption, no declared initial values, mode bmc, default depth 20, smtbmc yices, assert(count <= 9) as a clocked check. SBY reports the failure at which step?

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

ConceptWhich reset idiom is the wrong one?

always @(posedge clk) if ($initstate) assume(rst); else assume(!rst);A held-reset counter with assume(rst == (rst_cnt < 2))always @(posedge clk) assume(rst); with no $initstate guardA declared initial value on every flop, such as reg [3:0] count = 0;

ConceptWhy is an unreset flop a free variable to a formal tool?

It is X, and an X compares as false in every check the tool runs, so the assert fails.The tool randomises it at the start of every run, the way a simulator does with its seed.The tool ignores flops that have no reset and treats them as constant zero in every proof.Nothing constrains its first-step value, so the solver picks the value that breaks the property.

Read the waveformIn the strap trace, which value is a free choice of the solver and which is a consequence?

An unreset strap flop: free in step 0, then held

mode at step 0 is free; count from step 1 on is a consequence.count at step 0 is a consequence; mode is driven by the RTL.count from step 1 on is free; mode is a consequence.rst at step 0 is free; mode follows from it.

Remember

Reachability starts from the initial states; with nothing constraining them, every state is initial and a false property fails in step 0.
Say how the design starts: assume rst in the $initstate step, declare initial values, or hold the reset with a counter.
An unreset flop is a free choice in step 0 only; the solver picks the value that breaks the property.
A flop firmware initialises is an assumption to write down and review, or a reset to add in the RTL.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.