Counters, Timers and Shift Registers

Required Depth Comes First

A counter in the control path sets the depth a bounded run needs (F7.3). A property about expiry needs the timer to expire: step 65536 here, then one step to sample the bark and one to report it, so bmc needs depth 65539. Depth 40 says nothing about it.

The cover says the same thing in the tool's own words: cover(bark) comes back unreached within 40. Read that as a warning about the bound, not as dead logic.

Shrink the Counter Soundly

With four bits the bug appears at reported step 18: kick and expiry in the same cycle, and the bark one cycle later. The argument that carries this back to 16 bits is about the RTL, not the tool: the timer feeds only tmr == MAX.

The free route deletes the timer instead. An expired input chosen by the solver replaces it, with an assumption that it rises only after a kick-free cycle and a cover that it rises at all. Every real behaviour is still possible, so a PASS carries over to the real timer.

Induction Needs No Bound

"Bark only after an unkicked expiry" is about one transition, so induction proves it at k = 2 for the 16-bit timer. On the buggy design the induction step fails from a start with tmr = 65535 and kick = 1. Is that state reachable? Yes, after 65535 quiet cycles: you argue it, the tool cannot show it in budget.

A shift register is the same lesson in another shape. A 32-stage register needs 32 steps before its last stage sees the first input: cover(dout) is reached at reported step 34.

Asked in Interviews

Try It

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

assert property (@(posedge clk) disable iff (rst) bark |-> $past(tmr == MAX && !kick));
assert property (@(posedge clk) disable iff (rst) kick |=> tmr == 0);
cover property (@(posedge clk) disable iff (rst) bark);

  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg f_expire_q = 0, f_kick_q = 0;   // registered copies: last cycle's expiry and kick
  always @(posedge clk) begin
    f_expire_q <= !rst && tmr == MAX && !kick;
    f_kick_q <= !rst && kick;
  end
  always @(posedge clk) if (!rst) begin
    assert(!bark || f_expire_q);   // bark |-> $past(tmr == MAX && !kick)
    assert(!f_kick_q || tmr == 0); // kick |=> tmr == 0
    c_bark: cover(bark);
  end

1. Worksheet first

   For each width, write the required depth for cover(bark) before you run anything.

2. Run both widths

   16 bits at depth 40: BMC PASS to depth 40. 4 bits at depth 20: FAIL at reported step 18.

3. Prove

   Fix the bark, set the width back to 16 and run prove at k = 2: Prove PASS (k = 2). Write the soundness note that links the two results.

Check Yourself

module wdt16 #(parameter W = 16)(input clk, rst, kick, output reg bark = 0);
  localparam [W-1:0] MAX = {W{1'b1}};
  reg [W-1:0] tmr = 0;
  always @(posedge clk)
    if (rst) begin tmr <= 0; bark <= 0; end
    else begin
      tmr <= kick ? {W{1'b0}} : tmr == MAX ? MAX : tmr + 1'b1;   // holds at MAX until kicked
      bark <= tmr == MAX;            // bug: the kick term is missing
    end
`ifdef FORMAL
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  reg f_expire_q = 0, f_kick_q = 0;   // registered copies: last cycle's expiry and kick
  always @(posedge clk) begin
    f_expire_q <= !rst && tmr == MAX && !kick;
    f_kick_q <= !rst && kick;
  end
  always @(posedge clk) if (!rst) begin
    assert(!bark || f_expire_q);   // bark |-> $past(tmr == MAX && !kick)
    assert(!f_kick_q || tmr == 0); // kick |=> tmr == 0
  end
`endif
endmodule