Choosing a Depth

The depth of a bounded check is the one number that decides whether the check means anything. Too small, and the interesting behavior of the design never happens within the run, so every assertion passes vacuously. Too large, and the run is slow or times out. This article shows three practical ways to choose a depth: counting from the design, measuring with covers, and reasoning about the longest path from reset. A debouncer with an off-by-one bug shows all three.

9 min read | Intermediate

What You'll Learn

• Estimate the depth a check needs from reset latency, counters and pipeline stages
• Measure the depth with covers for the behaviors that matter
• Explain the reachability diameter and when a bounded check becomes complete
• Find a debouncer bug that appears only at depth 7 or more

The Design: a Debouncer

A mechanical button bounces: for a few milliseconds after a press, its contact opens and closes many times. A debouncer passes the input to its output only after the input has been stable for a number of cycles. This one should follow din after 4 stable cycles:

module debounce (input clk, input rst, input din, output reg dout);
  reg [2:0] cnt;
  always @(posedge clk)
    if (rst) begin
      cnt <= 3'd0; dout <= 1'b0;
    end else if (din == dout) begin
      cnt <= 3'd0;
    end else if (cnt == 3'd4) begin          // bug: should be 3
      dout <= din; cnt <= 3'd0;
    end else begin
      cnt <= cnt + 3'd1;
    end
endmodule

The counter counts the cycles in which din differs from dout. Comparing with 4 means it waits one cycle more than the specification allows.

The rule: once din has kept its value for 4 clock edges, dout equals it. A small helper, stab, counts how many edges in a row din has not changed:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // helper: for how many clock edges in a row din has kept its value
  reg       prev = 1'b0;
  reg [3:0] stab = 4'd0;
  always @(posedge clk) begin
    prev <= din;
    stab <= (rst || din != prev) ? 4'd0 : (stab == 4'd15 ? stab : stab + 4'd1);
  end
  // once din has been stable for 4 edges, dout has followed it
  always @(posedge clk) if (!init && stab >= 4'd4 && din == prev) assert (dout == din);
`endif

Method 1: Count From the Design

Add up the cycles the behavior needs, starting from reset:

• 1 cycle of reset.
• 4 edges with a stable new value on din.
• 1 cycle in which dout should have changed.
• 1 step for the clocked assertion to report.

That gives 7. The lab engine agrees: the buggy debouncer passes at depths 5 and 6 and fails at depth 7, in step 6.

Counting works well for blocks with clear latencies: timers, pipelines, protocol engines. The general recipe is: reset cycles, plus the longest counter or timeout the property depends on, plus pipeline stages between cause and effect, plus a few cycles of margin.

Method 2: Measure With Covers

A cover tells you exactly when a behavior first becomes possible. For the debouncer, cover the event the rule is about, "dout changes":

c_change: cover property (@(posedge clk) disable iff (rst) $changed(dout));

On the fixed design, SymbiYosys reports it reached in step 6. Any depth below 7 cannot contain a single change of dout, so every rule about such changes would pass vacuously. Covers turn depth from a guess into a measurement. Cover each behavior your assertions talk about, and set the depth above the largest reached step.

In the lab, use a meant-to-fail assertion, assert (dout == $past(dout)) with the usual guards: the step at which it fails is the same measurement.

Method 3: The Longest Path From Reset

Every reachable state has a shortest path from reset. The longest of these shortest paths is called the reachability diameter of the design. A bounded check whose depth is larger than the diameter has seen every reachable state, so for invariants it is as good as a full proof.

For small control blocks, the diameter is easy to estimate: for the debouncer it is a handful of cycles, because every state is reachable within a few steps. For a 32-bit counter it is over four billion. The diameter explains why BMC is complete for some blocks at small depths and hopeless for others, and why the deep bugs article and Chapter 6 exist.

Running It in ChipVerify Lab

The example below is the buggy debouncer with the stability helper and the rule. Run it at depth 6 and depth 7 and compare. Then fix the compare value to 3 and check that depth 10 passes.

Common Mistakes