Why Proofs Do Not Converge

The Cone of Influence

The cone of influence of an assertion is every signal that can reach it through gates and flops, back to the inputs. Tools delete everything else before an engine starts. What matters is what the cone contains, and how far back in time it reaches.

Three things stall a proof. Sequential depth: a counter puts behaviour thousands of cycles away. Hard logic in the cone: a multiplier, a wide compare. And a property that is not inductive (F2.4, F4.6). This watchdog has the first two.

Depth: The Bound Against the Bug

The shortest timeout is 256 × 256 = 65,536 cycles. The cut run below fails at step 4; on the real timer the same failure sits 65,536 steps later, so a bounded proof needs depth 65,541.

This is the proof-depth argument: derive the required bound from the deepest counter and the longest transaction before you trust a bounded PASS, and back it with covers. Here the expiry cover is unreached, so the runs never exercised the logic that matters.

Two Ways a Run Fails to Finish

The watchdog fails the first way: the bound is too deep to reach, and every affordable depth says PASS, which means nothing. The spine FIFO fails the second way: a modest depth is too slow to reach, and the run ends with no verdict at all.

Both are called "the proof does not converge", and they have different cures. A deep bound needs abstraction of the deep element (F4.2, F4.5). A slow solver needs an invariant (F4.6) or another engine (F4.7).

The Cone: What Every Step Carries

Each unrolled step copies the whole cone. To print PASS for the faulty design, the solver must show that timer never equals the product within 40 steps: arithmetic, in every copy. With a concatenated limit that claim is trivial. On the fixed design no failure depends on it, so the solver never asks.

Cut the Timer

wire expired = timer == pre_q * ticks_q;

wire expired = $anyseq;

A cut point makes expired a free input: any value in any cycle. Every behaviour of the real timer is still possible, plus more. In the trace the solver raises expired in the first RUN cycle together with a kick, and the FSM barks at step 3.

Is the failure real? It needs only a kick in an expiry cycle, which the real timer reaches after 65,536 cycles. So it is a real bug, found in 0.5 s. The last row shows k-induction never needed the timer's value at all. F4.2 shows a cut whose failure is false.

Asked in Interviews

Try It

The lab is the faulty watchdog, bmc at depth 20 with smtbmc yices. Measured: BMC PASS to depth 20, 1.2 s. The rule in concurrent SVA is shown first; the design carries its immediate form.

assert property (@(posedge clk) disable iff (rst)
  state == RUN && kick |=> !bark);

1. Read the claim

   Note what BMC PASS at depth 20 promises, and what the required bound is.

2. Cut the timer

   Replace the right side of wire expired = ... with $anyseq; and run again. Read the step where kick and expired are both 1.

3. Fix and prove

   Swap the two tests in the RUN branch so the kick wins, set mode prove and depth 2, and run with the cut and without it.

Check Yourself

module wdt(input clk, rst, start, kick, input [15:0] pre, ticks, output bark);
  localparam IDLE = 2'd0, RUN = 2'd1, BARK = 2'd2;
  reg [1:0] state = IDLE;
  reg [15:0] pre_q = 0, ticks_q = 0;
  reg [31:0] timer = 0;
  wire expired = $anyseq;                     // cut point: any value, every cycle
  assign bark = state == BARK;
  always @(posedge clk)
    if (rst) begin state <= IDLE; timer <= 0; end
    else case (state)
      IDLE: if (start) begin pre_q <= pre; ticks_q <= ticks; timer <= 0; state <= RUN; end
      RUN: if (expired) state <= BARK;     // bug: expiry tested first
           else if (kick) timer <= 0;
           else timer <= timer + 32'd1;
      default: if (kick) state <= IDLE;
    endcase
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(*) assume(pre >= 16'd256 && ticks >= 16'd256);   // the shortest timeout
  // a kick while running means no bark in the next cycle
  reg f_kick = 0;
  always @(posedge clk) begin
    f_kick <= !rst && state == RUN && kick;
    if (!rst && f_kick) assert(!bark);
  end
endmodule

module wdt(input clk, rst, start, kick, input [15:0] pre, ticks, output bark);
  localparam IDLE = 2'd0, RUN = 2'd1, BARK = 2'd2;
  reg [1:0] state = IDLE;
  reg [15:0] pre_q = 0, ticks_q = 0;
  reg [31:0] timer = 0;
  wire expired = timer == pre_q * ticks_q;
  assign bark = state == BARK;
  always @(posedge clk)
    if (rst) begin state <= IDLE; timer <= 0; end
    else case (state)
      IDLE: if (start) begin pre_q <= pre; ticks_q <= ticks; timer <= 0; state <= RUN; end
      RUN: if (expired) state <= BARK;     // bug: expiry tested first
           else if (kick) timer <= 0;
           else timer <= timer + 32'd1;
      default: if (kick) state <= IDLE;
    endcase
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(*) assume(pre >= 16'd256 && ticks >= 16'd256);   // the shortest timeout
  // a kick while running means no bark in the next cycle
  reg f_kick = 0;
  always @(posedge clk) begin
    f_kick <= !rst && state == RUN && kick;
    if (!rst && f_kick) assert(!bark);
  end
endmodule