Unreachable States and Induction Failures

The most common surprise in formal verification is an induction proof that fails on a design that is correct. A bounded check passes at any depth, a simulation never sees a problem, and yet the induction step reports a counterexample. The cause is almost always a state that reset can never reach. This article shows such a failure on a pair of lockstep counters, explains why a larger induction depth does not help, and how to recognize this kind of counterexample.

9 min read | Intermediate

What You'll Learn

• Recognize an induction counterexample that starts in an unreachable state
• Explain why the induction step considers such states at all
• Explain why raising k fixes some step failures and not others
• Tell a false induction failure from a real bug

The Design: Lockstep Counters

Safety-critical chips often run two copies of the same logic side by side and compare their outputs, so that a fault in one copy is detected. Here are two copies of a decimal counter:

module lockstep (input clk, input rst, input en, output done_a, output done_b);
  reg [3:0] a, b;
  always @(posedge clk)
    if (rst) begin
      a <= 4'd0; b <= 4'd0;
    end else if (en) begin
      a <= (a == 4'd9) ? 4'd0 : a + 4'd1;
      b <= (b == 4'd9) ? 4'd0 : b + 4'd1;
    end
  assign done_a = (a == 4'd9);
  assign done_b = (b == 4'd9);
endmodule

The property is what the comparator checks: both copies agree.

a_agree: assert property (@(posedge clk) disable iff (rst) done_a == done_b);

It is true. Both counters start at 0 and do the same thing in every cycle, so they are always equal. A bounded check at depth 20 passes, which covers every state of this small design.

The Induction Step Fails

In prove mode, the base case passes and the induction step fails:

SBY [run] engine_0.induction: ##   0:00:00  Trying induction in step 1..
SBY [run] engine_0.induction: ##   0:00:00  Trying induction in step 0..
SBY [run] engine_0.induction: ##   0:00:00  Temporal induction failed!
SBY [run] engine_0.induction: ##   0:00:00  Assert failed in lockstep: design.sv:19.26-19.51
SBY [run] summary: engine_0 (smtbmc bitwuzla) returned pass for basecase
SBY [run] summary: engine_0 (smtbmc bitwuzla) returned FAIL for induction
SBY [run] summary: counterexample trace [induction]: run/engine_0/trace_induct.vcd
SBY [run] DONE (UNKNOWN, rc=4)

Note the final status: UNKNOWN, not FAIL. The tool found no real bug, and it could not prove the property either. The induction trace, from a run with k = 3, shows why:

The step starts with a = 6 and b = 14. For three cycles done_a and done_b are both 0, so the property holds, as the step requires. Then a reaches 9 and b is 1: the two disagree. This start state is impossible after reset, where a and b are always equal. But nothing in the property rules it out, because the property only talks about done_a and done_b, not about a and b.

Why a Larger k Does Not Help

A larger induction depth demands more good cycles before the bad one. That sometimes helps: if the unreachable states can only "pretend" to be good for a cycle or two, a larger k rules them out. Here it does not. On the lab engine, the step fails with k = 2, 5, 10 and 20.

The unreachable states with a different from b form long chains in which done_a and done_b both stay 0. The counter can also stand still when en is low, so such a state can stay good for as many cycles as k demands, and then step into disagreement. No value of k excludes them.

The decimal counter from the previous article showed the same effect: the step for q != 11 started at the unreachable value 10, held it with en low, and then counted to 11.

False Failure or Real Bug?

Every induction counterexample needs this decision:

• Is the start state reachable? If it violates a relation that holds after reset, it is not, and the failure is false.
• Does the base case pass at a depth that covers the trace? If the same sequence can happen from reset, the base case finds it as a real counterexample.
• Does a bounded run of the suspected relation pass? Assert a == b in a normal run. If it passes, the relation is a candidate helper property.

A false failure is not a reason to give up. It tells you which relation the tool is missing, and adding that relation is the subject of the strengthening invariants article.

Running It in ChipVerify Lab

The example below runs the induction step for the lockstep counters in the lab form, with k = 4:

`ifdef FORMAL
  // induction step in the lab: start anywhere, never reset
  always @(*) assume (!rst);
  reg [7:0] step = 8'd0;
  always @(posedge clk) step <= step + 8'd1;
  // the properties hold in the first K steps ...
  always @(*) if (step < 8'd4) assume (done_a == done_b);
  // ... and must still hold in step K
  always @(*) if (step == 8'd4) assert (done_a == done_b);
`endif

Run at depth 5 or more. It fails at step 4, with a and b starting at different values.

Common Mistakes