State Explosion and the Cone of Influence

A design with n bits of state has up to 2ⁿ states. Add one 32-bit register and the state space grows four billion times. This is called state explosion, and it is the reason formal tools work on blocks, not chips. Yet the size of the design alone does not decide whether a check finishes. This article explains what really matters, shows the cone of influence that every tool uses automatically, and gives an overview of the techniques in this chapter.

8 min read | Intermediate

What You'll Learn

• Explain state explosion and why it does not always hurt
• Describe the cone of influence of a property and how tools use it
• Predict which properties of a design will be easy and which hard
• Choose a technique from this chapter for a check that does not finish

State Explosion

The state and reachability article showed how the state space doubles with every register bit. Bounded model checking does not enumerate those states, it hands a formula to a solver. Still, the formula grows with the number of bits that matter, and some kinds of logic make it very hard to solve. The performance article measured a multiplier check that took 15 seconds at 8 bits and more than 300 at 10.

Two observations make the problem manageable. First, most properties depend on a small part of the design. Second, most of the hard logic, such as wide arithmetic, does not matter for most properties.

The Cone of Influence

The cone of influence of a property is the set of signals and registers that can affect it, directly or through any chain of logic, at any time. Everything outside the cone cannot change the outcome, so tools remove it before solving. Yosys and SymbiYosys do this as part of their normal optimization.

The effect can be dramatic. The shift-and-add multiplier from the performance article has two kinds of property:

• Control: done comes exactly W cycles after a start. Its cone contains the start logic and the cycle counter, not the product.
• Data: the product equals a * b. Its cone contains the whole datapath.

On the lab engine, the control property passes at 12 bits in under a second, and at 32 bits in about a second too. The data property times out at 10 bits. Same design, same depth, completely different difficulty, because the cones differ.

What Makes a Cone Hard

• Arithmetic compared with arithmetic: a product checked against a different product, or a divider against a multiplication.
• Deep sequential depth: counters and timeouts whose interesting values are many cycles from reset.
• Many interacting registers: large state machines, long pipelines with feedback, caches.
• Large memories with complex addressing, although simple read-after-write checks are cheap.

The Techniques of This Chapter

All of them make the problem smaller while keeping the result meaningful. Each has a condition for being sound, and each article states it.

Running It in ChipVerify Lab

The example below is the shift-and-add multiplier with the control property only, at W = 6, which needs a depth of 10. A job takes W cycles, so wider versions need more depth: with PRO, try W = 12 at depth 16 and W = 32 at depth 36. The time barely changes. Compare with the data property in the performance example.

`ifdef FORMAL
  // ... reset ...
  // control only: done comes exactly W cycles after a start
  reg [7:0] since = 8'd0; reg running = 1'b0;
  always @(posedge clk)
    if (rst) running <= 1'b0;
    else if (start && !busy) begin running <= 1'b1; since <= 8'd0; end
    else if (running) begin since <= since + 8'd1; if (done) running <= 1'b0; end
  always @(posedge clk) if (!init && done) assert (running && since == W);
`endif

Common Mistakes