Performance

Some formal runs finish in a second, others never finish. The difference rarely comes from the number of lines of RTL. It comes from what the logic does: wide arithmetic, deep counters, large state, and the depth of the run. This article measures run times on the lab engine for a multiplier of growing width, compares the three engines, and lists the levers you have when a run is too slow.

9 min read | Intermediate

What You'll Learn

• Name the features of a design that make formal runs slow
• Explain why wide multiplication is hard for a solver while memories and shifters are often easy
• Compare the engines of the lab on one hard design
• Choose a technique to speed up a run that times out

What Makes a Run Slow

• Depth. Every cycle adds a copy of the logic, as the unrolling article showed.
• Wide arithmetic. Multipliers, dividers and wide adder trees produce formulas that solvers find very hard, and the effort grows steeply with the width.
• Many state bits that interact. Large counters, many registers feeding each other, and long pipelines enlarge the space the solver must reason about.
• Properties that need the whole design. An end-to-end property across many modules forces the solver to consider all of them together.

Some things that look large are cheap. A memory of 256 entries checked with a tracked address took about as long as one of 4 entries on the lab engine, because the solver handles memory as an array instead of 256 separate registers. A 16-bit shift register with a property at depth 100 finished in under a second. Size in lines or bits is a poor predictor. The kind of logic matters more.

A Hard Case: Multiplication

This multiplier computes a product one bit at a time, the classic shift-and-add method, and the property compares the result with a * b:

module seqmul #(parameter W = 6) (input clk, input rst, input start, input [W-1:0] a, input [W-1:0] b,
                                 output reg done, output reg [2*W-1:0] p);
  reg [2*W-1:0] ma;
  reg [W-1:0]   mb;
  reg [7:0]     n;
  reg           busy;
  always @(posedge clk)
    if (rst) begin
      busy <= 1'b0; done <= 1'b0;
    end else if (start && !busy) begin
      ma <= a; mb <= b; p <= 0; n <= 0; busy <= 1'b1; done <= 1'b0;
    end else if (busy) begin
      if (mb[0]) p <= p + ma;
      ma <= ma << 1; mb <= mb >> 1; n <= n + 8'd1;
      if (n == W - 1) begin busy <= 1'b0; done <= 1'b1; end
    end else
      done <= 1'b0;
endmodule

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // remember the operands of the job
  reg [W-1:0] ra, rb;
  always @(posedge clk) if (start && !busy && !rst) begin ra <= a; rb <= b; end
  // when done, the product is a * b
  always @(posedge clk) if (!init && done) assert (p == ra * rb);
`endif

The design is correct. Its check is a question every solver struggles with: are two different ways of multiplying the same for all inputs? The run times on the lab engine, with a depth of the width plus 4:

Each two extra bits multiply the time many times over. At 10 bits the run hits the lab limit of 300 seconds. A 32-bit multiplier checked this way would never finish. This is why datapaths with arithmetic are usually checked by other means, as the next sections show.

The Engines

On the 8-bit multiplier, the three engines of the lab took:

Bitwuzla and Boolector are close, as on most bit-level designs. Z3 is often slower on such logic, as it was on the mod-60 counter in Chapter 2. The ranking can change from design to design, so trying another engine is a cheap first step when a run is slow, but no engine turns an exponential problem into an easy one.

Levers for a Slow Run

• Lower the depth to what the property needs, using the methods of the choosing a depth article.
• Shrink the design with parameters: narrower data, fewer entries, shorter counters. The 6-bit multiplier keeps the logic of the 32-bit one.
• Remove what the property does not need: black boxes and cut points replace logic that does not matter for a property with free inputs. Chapter 8 covers these.
• Split end-to-end properties into properties per module, with assume-guarantee at the boundaries.
• Treat arithmetic separately: check the control logic around a datapath formally, with the arithmetic cut out, and check the arithmetic by simulation against a reference model or with equivalence checking against a known-good version.
• Prove instead of unrolling: an induction proof needs only a few frames, so it can be faster than a deep bounded run. Chapter 6 shows how.

Running It in ChipVerify Lab

The example below is the shift-and-add multiplier with W = 6, which passes in seconds. Change the parameter to 8 and run again, then try the other engines. With PRO, try 10 bits and watch the run hit the time limit.

Common Mistakes