How BMC Unrolls a Design

Bounded model checking turns a question about a circuit over time into a single question for a solver. It does this by unrolling: it copies the logic of the design once for every clock cycle it wants to examine and chains the copies together. This article explains unrolling step by step, connects it to the log lines you have seen in every run, and shows why the depth decides both what a run can find and how long it takes.

9 min read | Intermediate

What You'll Learn

• Describe how BMC unrolls a design into one copy of its logic per clock cycle
• Explain the parts of the formula: start state, transition, free inputs and the property
• Read the step-by-step lines of a SymbiYosys log in terms of unrolling
• Relate the step at which a state first appears to its distance from reset

A Design Is State Plus Logic

Every synchronous design can be split into two parts. The registers hold the state. The combinational logic computes, from the current state and the current inputs, the next state and the outputs. At each clock edge, the registers load the next state. The state and reachability article introduced this view.

For a formal tool, the combinational logic is a function, often called the transition relation: given state s and inputs i, it gives the next state. That function is all the tool needs to know about the design.

Unrolling

To look at k clock cycles, BMC writes down k copies of the combinational logic, one per cycle, called frames. The registers disappear: the next-state output of frame 0 is wired straight to the state input of frame 1, and so on. Every frame gets its own copy of the inputs, which the solver may choose freely.

The formula given to the solver says:

• The state in frame 0 is a legal start state: the reset assumption holds.
• Each frame follows from the previous one through the logic of the design.
• All assumptions hold in every frame.
• The property is false in at least one frame.

If the solver finds values that make all of this true, those values are the counterexample: the inputs of every frame form the waveform. If no such values exist, no input sequence of length k breaks the property.

What the Log Shows

SymbiYosys does not build the whole formula at once. It adds one frame at a time and asks the solver after each one:

SBY [run] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY [run] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY [run] engine_0: ##   0:00:00  Checking assumptions in step 1..
SBY [run] engine_0: ##   0:00:00  Checking assertions in step 1..
...

"Checking assumptions in step n" adds frame n and makes sure the assumptions can still be met. If they cannot, the run stops with "Assumptions are unsatisfiable!", as the over-constraining article showed. "Checking assertions in step n" asks whether any assertion can fail in frame n. The first step where the answer is yes becomes the counterexample, so counterexamples are always as short as possible.

The solver keeps what it learned about the earlier frames, so each new step builds on the previous ones. This is called incremental solving and is why a run of depth 20 is usually much cheaper than twenty separate runs.

Distance From Reset

Because the tool checks frame by frame, the step at which a state first appears in a counterexample is the minimum number of cycles needed to reach it from reset. That makes BMC a precise way to measure distances inside a design.

Take a 16-bit linear feedback shift register (LFSR), a shift register whose input is the XOR of some of its own bits. It is used to generate pseudo-random numbers and test patterns:

module lfsr16 (input clk, input rst, input en, output reg [15:0] s);
  wire fb = s[15] ^ s[13] ^ s[12] ^ s[10];
  always @(posedge clk)
    if (rst)     s <= 16'h0001;
    else if (en) s <= {s[14:0], fb};
endmodule

After reset the single 1 moves up one bit per enabled cycle, as long as the feedback is 0. Ask the tool for the first time s equals 16'h0080 by asserting that it never does: assert (s != 16'h0080). The run fails at step 9: reset in step 0, then 1 in step 1, and the 1 reaches bit 7 in step 8, reported at the next edge. Ask for 16'h0100 instead and depth 10 passes, because that value needs one more cycle. At depth 11 it fails at step 10.

Why Depth Costs Time

Each frame is a full copy of the logic, so the formula grows linearly with the depth. The time the solver needs can grow much faster, because it reasons about all frames together. For a small design such as the LFSR, even depth 100 finishes in about a second on the lab engine. For designs with wide arithmetic, every frame contains a large multiplier or adder, and the time can explode with a few more frames. The performance article measures this.

Running It in ChipVerify Lab

The example below is the LFSR with the property that it never reaches the all-zero state, which would lock it up. That property holds for this LFSR, so the run passes at any depth. Use it to explore distances: change the asserted value and watch the failing step move.

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

Common Mistakes