Induction: Base Case and Step

Induction is how a formal tool proves that a property holds in every cycle without looking at every cycle. It splits the job into two small checks: the property holds at the start, and a good state can never be followed by a bad one. This article explains both checks with a decimal counter, shows the output of SymbiYosys in prove mode, and shows how to run the induction step in ChipVerify Lab.

9 min read | Intermediate

What You'll Learn

• Explain the base case and the induction step of k-induction
• Read the prove-mode log of SymbiYosys
• Explain why the step starts from an arbitrary state, not from reset
• Run the induction step as a bounded check in the lab

The Idea

Induction replaces "check every cycle" with two checks that are each small, and that together cover every cycle:

• Base case: starting from reset, the property holds in the first k cycles. This is exactly a bounded check of depth k.
• Induction step: take any k consecutive cycles in which the property holds, starting from any state at all. Then the property also holds in the next cycle.

If both checks pass, the property holds forever: the first k cycles are good by the base case, and each later cycle is good because the k cycles before it were. The number k is the induction depth. With k = 1 it is the classic induction from mathematics.

Why the Step Starts Anywhere

The step does not start from reset, because then it would only cover the first cycles again. It starts from any state that satisfies the property for k cycles, reachable or not. That is what makes it independent of depth: the solver does not walk from reset, it only looks at k + 1 consecutive cycles somewhere.

The price is that the step also considers states that reset can never produce. If one of those good-looking states can step into a bad one, the step fails even though the design is correct. The next article is about exactly that.

An Example: the Decimal Counter

module mod10 (input clk, input rst, input en, output reg [3:0] q);
  always @(posedge clk)
    if (rst)     q <= 4'd0;
    else if (en) q <= (q == 4'd9) ? 4'd0 : q + 4'd1;
endmodule

The property: the counter always shows a decimal digit.

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

The induction step with k = 1 asks: if q is at most 9 in one cycle, can it be more than 9 in the next? Look at the logic: from 9 it goes to 0, from 0 to 8 it goes up by one, and without en it stays. None of these leaves the range. So the step holds, and with the base case the property is proven for every cycle.

The Prove-Mode Log

SymbiYosys runs the two checks as two processes, basecase and induction, when its mode is prove:

SBY [run] engine_0.basecase: ##   0:00:00  Checking assumptions in step 0..
SBY [run] engine_0.basecase: ##   0:00:00  Checking assertions in step 0..
SBY [run] engine_0.basecase: ##   0:00:00  Status: passed
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 successful.
SBY [run] summary: engine_0 (smtbmc bitwuzla) returned pass for basecase
SBY [run] summary: engine_0 (smtbmc bitwuzla) returned pass for induction
SBY [run] summary: successful proof by k-induction.
SBY [run] DONE (PASS, rc=0)

The depth setting of a prove-mode run is the induction depth k. Here it was 1, and both checks passed in well under a second.

Running It in ChipVerify Lab

The lab panel only runs bounded checks, but both halves of an induction proof can be written as bounded checks:

• The base case is the normal lab run with the reset assumption, at a depth of at least k.
• The induction step is a run without any reset, where the property is assumed for the first k steps and asserted in step k.

For the counter with k = 1, the step looks like this:

`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'd1) assume (q <= 4'd9);
  // ... and must still hold in step K
  always @(*) if (step == 8'd1) assert (q <= 4'd9);
`endif

Without a reset, q starts at whatever value the tool chooses, limited only by the assumption. The step register is formal-only helper logic that counts the cycles, and its initial value of 0 is honored by the formal tool. Run it at depth 2 or more: it passes, so the step holds. Together with the normal lab run, which passes from reset, that is a complete proof.

Common Mistakes