Shrinking the Problem

Most designs have sizes: data width, number of entries, counter width, number of channels. Formal difficulty often grows steeply with them, while the logic that matters stays the same. Shrinking means checking a smaller configuration of the same design, through its parameters, so the check finishes. This article measures how a FIFO check scales with its width and depth on the lab engine, and shows which reductions are safe and what to do when even the small check is not enough.

8 min read | Intermediate

What You'll Learn

• Shrink a design through its parameters without changing its logic
• Predict which size parameter drives the cost of a check
• Decide when a shrunk result transfers to the full size
• Use induction to remove the depth that large sizes demand

Shrinking Through Parameters

If every size in the RTL comes from a parameter, the formal setup can choose small values: a 4-entry FIFO instead of 64, 8-bit data instead of 64, a 4-bit timeout counter instead of 20. The control logic is the same code, so most bugs in it appear in the small version too, and much sooner. The deep bugs article used this to find a watchdog wrap in 6 steps instead of 1024.

The precondition is design discipline: no hard-coded constants that should follow a parameter, no special cases that only exist at the full size. Reviews for formal readiness check exactly this.

What Drives the Cost

The FIFO from the FIFO capstone, with flag checks against a reference count and a tracked-value order check, at several sizes. The bounded depth is chosen so the FIFO can be filled: a few cycles more than the number of entries.

• Data width costs little: 1, 8 and 32 bits at 4 entries take 2, 4 and 8 seconds. The FIFO is data independent, and the tracked value only needs to be told apart from other words.
• Number of entries costs a lot, directly and through the depth needed to fill the FIFO: 8 entries already time out at 300 seconds, even with 8-bit data, and 16 entries time out even with 1-bit data.

So for a FIFO, shrink the depth of the memory first. The data width can often stay realistic.

When Does a Small Result Transfer?

A check of the 4-entry FIFO says nothing, formally, about 1024 entries. It transfers in practice when:

• the logic is the same code, with sizes from parameters only;
• nothing in the design behaves differently at specific sizes, such as power-of-two optimizations or special full-size handling;
• the small size still reaches every interesting situation: full, empty, wrap-around, simultaneous push and pop.

Covers at the small size confirm the last point. Some bugs depend on size, such as an overflow of a counter that is too narrow for the full depth, so shrinking is combined with a few targeted checks at the real size.

Induction Removes the Depth

A bounded check must unroll enough cycles to fill the FIFO, which is what makes large sizes expensive. An induction proof does not: with the right helper invariants, the step looks at a single cycle from any state. On the lab engine, the FIFO capstone's proof with its three helpers passes with k = 1 for 4 entries, for 16 entries of 32 bits, and for 64 entries of 32 bits, each in under a second. The sizes that defeated the bounded check are no problem for the proof.

The usual workflow combines both: shrink to find bugs quickly and to develop the helpers, then prove at the real size.

Running It in ChipVerify Lab

The example is the parameterized FIFO with flag and order checks, at W = 8 and AW = 2 (4 entries). Run it at depth 10. Then change W to 32 and run again; with PRO, try AW = 3 at depth 20 and watch the run hit the time limit.

Common Mistakes