Induction Strengthening in Practice

The Recipe

k-induction fails when an unreachable state that satisfies every assertion leads to a bad one (F2.4). The induction trace hands you that state as step 0. Find the relation that reset always keeps and step 0 breaks: that is the next helper.

Write the helper as an assertion, so the same run proves it. Repeat until PASS. If step 0 could be reached from reset, the base case will find the failure at a larger depth: then it is a bug, not a missing helper.

Round 1

Depth alone does not help: the start state can sit still for any number of steps. PDR finds an invariant by itself (F2.5), but the recipe gives you one you can read, review and reuse.

Round 2: The Trace Moves

The new start obeys round 1 (4 + 0 ≤ 4) but holds a credit in the return pipeline: r2 = 1. One cycle later the sender has five credits. The true invariant counts every unit of space wherever it is: with the sender, in the buffer, or on the way back.

With cred + occ + r1 + r2 == 4 the proof closes at depth 2, and round 1’s helper is implied (the second alone: Prove PASS, 0.5 s). The faulty twin returns a credit for an empty pop: FAIL at step 3, 0.5 s (bmc 12), on the round-2 helper, before any overflow.

The Spine FIFO, Closed

Step 0 of the plain induction trace has count 1 with the scoreboard holding 0: the ring and the shadow copy disagree. The invariants state what the design already does: the counts match, and each occupied ring slot holds its scoreboard byte.

assert(count == sb_n);
if (count > 3'd0) assert(mem[rd_ptr] == sb0);
if (count > 3'd1) assert(mem[rd_ptr + 2'd1] == sb1);
if (count > 3'd2) assert(mem[rd_ptr + 2'd2] == sb2);
if (count > 3'd3) assert(mem[rd_ptr + 2'd3] == sb3);

Back to the FIFO of F2.4

With count <= 16 alone, step 0 has count 1 and equal pointers, which breaks count == wr_ptr - rd_ptr. With that relation alone the proof closes. Add what step 0 breaks; extra helpers cost review time and can slow the solver.

Asked in Interviews

Try It

The lab is the credit counter in prove mode, depth 2, smtbmc yices. Measured: UNKNOWN at depth 2, 0.5 s.

assert property (@(posedge clk) disable iff (rst) occ <= 4);

1. Round 1

   Read step 0 of the induction trace. How many units of space do the credits and the buffer hold together? Assert the bound.

2. Round 2

   Run again. Which register in the new step 0 holds space that round 1 did not count? Assert the exact total.

3. Soundness

   Make the receiver return a credit on every pop request (r1 <= pop;) and run bmc at depth 12.

Check Yourself

module crd(input clk, rst, want, pop, output send);
  reg [2:0] cred = 3'd4;      // sender credits
  reg [2:0] occ = 3'd0;       // receiver buffer, four entries
  reg r1 = 0, r2 = 0;         // credit return pipeline
  assign send = want && cred != 3'd0;
  wire do_pop = pop && occ != 3'd0;
  always @(posedge clk)
    if (rst) begin cred <= 3'd4; occ <= 0; r1 <= 0; r2 <= 0; end
    else begin
      cred <= cred - send + r2;
      occ <= occ + send - do_pop;
      r1 <= do_pop; r2 <= r1;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  wire [3:0] f_sum1 = cred + occ, f_sum = cred + occ + r1 + r2;
  always @(posedge clk) if (!rst) begin
    assert(occ <= 3'd4);
  end
endmodule

module crd(input clk, rst, want, pop, output send);
  reg [2:0] cred = 3'd4;      // sender credits
  reg [2:0] occ = 3'd0;       // receiver buffer, four entries
  reg r1 = 0, r2 = 0;         // credit return pipeline
  assign send = want && cred != 3'd0;
  wire do_pop = pop && occ != 3'd0;
  always @(posedge clk)
    if (rst) begin cred <= 3'd4; occ <= 0; r1 <= 0; r2 <= 0; end
    else begin
      cred <= cred - send + r2;
      occ <= occ + send - do_pop;
      r1 <= do_pop; r2 <= r1;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  wire [3:0] f_sum1 = cred + occ, f_sum = cred + occ + r1 + r2;
  always @(posedge clk) if (!rst) begin
    assert(occ <= 3'd4);
    assert(f_sum1 <= 4'd4);               // round 1
  end
endmodule