Deep Bugs

Some bugs need hundreds or thousands of cycles from reset before they show: a timeout counter that misbehaves when it wraps, a statistics counter that overflows, a credit counter that drifts by one every thousand transactions. No affordable depth reaches them. This article shows a watchdog with such a bug, why a run at depth 100 passes it, and three ways to find it anyway: scaling the design down, starting from an arbitrary state, and full proofs.

9 min read | Intermediate

What You'll Learn

• Recognize properties whose failures need more cycles than BMC can afford
• Shrink a design with parameters so a deep bug becomes shallow
• Start a check from an arbitrary state instead of reset, and know its risk
• Decide which technique fits which kind of deep bug

The Design: a Watchdog Timer

A watchdog raises tout if software has not "kicked" it for 1000 cycles. The timeout must stay high until the next kick, so that a stuck system is reset for sure:

module timeout (input clk, input rst, input kick, output tout);
  reg [9:0] cnt;
  assign tout = (cnt >= 10'd1000);
  always @(posedge clk)
    if (rst || kick) cnt <= 10'd0;
    else             cnt <= cnt + 10'd1;   // bug: keeps counting and wraps after 1023
endmodule

The counter does not stop at 1000. After 1023 it wraps to 0 and tout drops, although no kick came. A stuck system would get a timeout pulse of 24 cycles instead of a steady signal.

The rule:

a_hold: assert property (@(posedge clk) disable iff (rst) tout && !kick |=> tout);

Why BMC Misses It

From reset, the counter needs 1024 cycles without a kick to wrap. A run at depth 100, the PRO maximum, passes in a few seconds, and the result is correct for what it checked: no failure within 100 cycles. The bug is simply 900 cycles beyond the horizon. Raising the depth to 1030 would find it in principle, but the run time grows with every frame, and most real deep bugs are much deeper than this one.

Technique 1: Scale the Design Down

The bug does not depend on the numbers 1000 and 1023. It is about what happens when the counter reaches its maximum. Make the width and the limit parameters, and check a small version:

module timeout #(parameter W = 10, parameter [W-1:0] LIMIT = 1000) (input clk, input rst, input kick, output tout);
  reg [W-1:0] cnt;
  assign tout = (cnt >= LIMIT);
  always @(posedge clk)
    if (rst || kick) cnt <= 0;
    else             cnt <= cnt + 1'b1;   // bug: keeps counting and wraps
endmodule

With W = 2 and LIMIT = 2, the counter wraps after 3 and the run fails at step 6, well inside the free depth. With W = 4 and LIMIT = 10 it fails at step 18. The fix, counting only while tout is low, passes for every size.

Scaling down is the most common technique in practice, for counters, FIFOs, memories and buses. Its limitation is that some bugs depend on the exact numbers, such as a comparison with a hard-coded constant that does not scale with the parameter. Design the RTL so that every size-dependent value comes from a parameter, and the small version keeps the logic of the big one.

Technique 2: Start Anywhere

The bug is deep only because the check starts at reset. Remove the reset assumption, and the tool may start the counter at any value, including 1023:

Now the run fails at step 2 on the full 10-bit design:

The tool starts with cnt = 1023, so tout is high, and one step later the counter has wrapped and tout is low. With the fix, the same start-anywhere run passes.

The risk is false failures. A free start state may be one that the design can never reach from reset. Here every count from 0 to 1023 is reachable, so any failure is real. In a design with unreachable states, the tool may start in one of them and report a failure that cannot happen. The usual remedy is to add assumptions or, better, proven invariants that rule out the unreachable start states. That is exactly the problem of induction, and Chapter 6 is about it.

Technique 3: Prove It for Every Depth

A full proof by induction checks every state that satisfies the properties, not just the states within a depth. For the watchdog, induction would find the wrap in one step, like the start-anywhere run, and would prove the fixed design for all time. Chapter 6 shows how.

Which Technique When

Running It in ChipVerify Lab

The example below is the 10-bit watchdog. Its formal block starts from reset:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  // start from reset: the bug is more than 1000 cycles away
  always @(*) if (init) assume (rst);
  // once tout is high, it stays high until a kick or reset
  always @(posedge clk) if (!init && !$past(rst) && $past(tout) && !$past(kick)) assert (tout);
`endif

Run it at depth 10, and with PRO at depth 100: both pass. Then delete the assume (rst) line to start anywhere, and the run fails at step 2.

Common Mistakes