Depth, Engines and Limits

Two settings in the formal panel decide what a run can find and how long it takes: the depth and the solver engine. A depth that is too small misses bugs without any warning, and a depth that is too large can make a run slow or time out. This article shows both effects on a counter whose bug needs 62 cycles to appear, and explains the limits of the lab engine.

8 min read | Beginner to Intermediate

What You'll Learn

• Explain why a bounded check passes when a bug needs more cycles than the depth
• Work out the depth a bug needs from the design
• Choose between the Bitwuzla, Boolector and Z3 engines
• Make a deep bug reachable at a small depth by scaling the design down

The Design: A Mod-60 Counter

A counter for the seconds of a clock counts from 0 to 59 and wraps to 0. This one has the same mistake as the counter in the first article: it compares with the wrong value, so it shows 60 for one count before it wraps.

module mod60 (input clk, input rst, input en, output reg [5:0] q);
  always @(posedge clk)
    if (rst)     q <= 6'd0;
    else if (en) q <= (q == 6'd60) ? 6'd0 : q + 6'd1;   // bug: should wrap at 59
endmodule

The rule: the count is never larger than 59.

a_60: assert property (@(posedge clk) disable iff (rst) q <= 6'd59);

In the lab form:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init) assert (q <= 6'd59);
`endif

A Pass That Means Little

Run the check at depth 10, the maximum on the free tier. It passes. That is correct for what was asked: no input sequence of 10 cycles can push the counter above 59, because the counter can count at most once per cycle. After a reset in step 0, the fastest it can go is 1 in step 2, 2 in step 3, and so on. In 10 cycles it reaches 8 at the most.

The bug is still there. It is simply out of reach. The value 60 first appears in step 61 (a reset cycle, then 60 counts), and the clocked assertion reports it at the next edge, step 62. A depth of 10 cannot see it.

Working Out the Depth a Bug Needs

For a counter, the depth follows from simple counting. A run with depth N checks steps 0 to N - 1. The failure here is reported in step 62, so the run needs a depth of at least 63. On the lab engine:

The step between 62 and 63 is the whole difference between "no bug" and "bug". Nothing in the passing runs warns you that a bug lies just beyond the depth. This is the main limitation of bounded model checking, and the reason the depth must be chosen from the design, not from habit.

A useful rule: the depth must be larger than the number of cycles the design needs to reach every interesting state from reset. For counters, timers and FIFOs that is roughly their largest count, plus a few cycles for the reset and the check. Chapter 5 shows how to measure it, and Chapter 6 shows how to prove a rule for any number of cycles, which removes the problem completely.

The Engines

The depth decides what can be found. The engine decides how fast. The formal panel offers three solvers. All of them answer the same question and give the same result on a correct run. They differ in speed, and the best one depends on the design.

• Bitwuzla is the default. It is a modern solver for bit-vectors, the kind of values that registers and buses hold, and it is the best first choice for most designs.
• Boolector is the older solver from the same research group. It is often about as fast as Bitwuzla on small designs.
• Z3 is a general-purpose solver. It handles complex arithmetic well but is often slower on plain control logic.

On the mod-60 counter at depth 70, all three find the same counterexample in step 62. Bitwuzla and Boolector finish in under a second, and Z3 takes about 7 seconds. On a larger design the gap can grow from seconds to minutes. If a run is slow, try another engine before you give up on it.

Limits of the Lab Engine

• Depth: up to 10 cycles on the free tier and up to 100 with PRO. The default is 10 on the free tier and 20 with PRO.
• Time: a run stops after 300 seconds. The lab then reports a timeout and suggests a smaller depth. The time a run needs grows quickly with the depth and the size of the design.
• Mode: the panel runs bounded model checking only. It reports PASS or a counterexample within the depth. Full proofs and cover traces are shown in this tutorial as tool output.
• Language: immediate assert, assume and cover in always blocks, $past and $stable, but no concurrent SVA and no bind.
• Cached results: the lab remembers the result of an identical run. The Cache button in the panel clears it if you want a fresh run.

Reaching a Deep Bug at a Small Depth

The mod-60 bug needs 63 cycles of depth only because 59 is a large number. The logic of the bug is the same for any wrap value. If the limit is a parameter, the formal check can use a small value, and the bug appears within a few cycles:

module mod60 #(parameter MAX = 6'd59) (input clk, input rst, input en, output reg [5:0] q);
  always @(posedge clk)
    if (rst)     q <= 6'd0;
    else if (en) q <= (q == MAX + 6'd1) ? 6'd0 : q + 6'd1;   // bug: should wrap at MAX
  // ... same `ifdef FORMAL block, with assert (q <= MAX)
endmodule

With MAX = 59 the run at depth 10 passes, as before. With MAX = 5 it fails at step 8, well inside the free depth, and the counterexample shows the same mistake. After the fix both values pass. Scaling a design down like this is a standard formal technique for counters, FIFOs and memories, and Chapter 8 covers it in detail.

Running It in ChipVerify Lab

The example below is the mod-60 counter with the bug. On the free tier, run it at depth 10 and see it pass. With PRO, run at depth 62 and 63 and compare, then try all three engines at depth 70.

Common Mistakes