Datapaths: Why Multipliers Hurt

The Curve

Each extra bit multiplies the time. Bit-level SAT takes 1.4 s at 7 bits and 18.0 s at 8, then passes the 20 s budget at 9. The word-level runs last longer: Yices to 9 bits, Bitwuzla to 10.

Two or three bits of headroom is all a better solver bought. At 32 bits the same growth means no answer on any machine.

Why Multipliers in Particular

Bryant proved in 1986 that the BDD of a multiplier's middle output bit is exponential in the width for every variable order. The comparator BDD of F2.6 fits on a page; the multiplier's outgrows practical memory somewhere in the mid-teens of bits.

SAT does not store the function, but it searches it. Here one side is * and the other a chain of shifted adds, so the solver finds little shared structure to learn from (F2.2).

What a Word-Level Solver Changes

module mul(input [3:0] a, b, output [7:0] p);
  assign p = a * b;
endmodule

module mul(input [3:0] a, b, output reg [7:0] p);
  integer i;
  always @* begin   // the shift-add multiplier of F2.2, unrolled: one partial product per bit of b
    p = 0;
    for (i = 0; i < 4; i = i + 1)
      if (b[i]) p = p + ({4'd0, a} << i);
  end
endmodule

An SMT solver sees * as one operation and can rewrite it when both sides are alike. Here the sides differ, so it lowers the multiply to gates internally and the problem returns to SAT. It starts later and climbs the same way.

Bitwuzla held out one bit longer than Yices on this pair. That ordering is a property of this design, not of the solvers, so measure on your own block before choosing an engine (F4.7).

Change the Question

Width reduction (F4.5) is the trap: a 4-bit multiplier proof says nothing about the carry chains of a 32-bit one. When a check will not finish, decompose it.

A decomposition is only sound if the pieces cover the whole. Prove each partial product against its slice of the reference, then prove the adder tree sums its inputs. Together the two proofs cover the multiplier with no single hard cone.

Asked in Interviews

Try It

[gold]
read_verilog -sv design.sv
prep -top mul

[gate]
read_verilog -sv gate.sv
prep -top mul

[strategy sby]
use sby
depth 1
engine smtbmc yices

[gold]
read_verilog -sv ref.sv
prep -top mul

[gate]
read_verilog -sv sa.sv
prep -top mul

[strategy sat]
use sat

1. Run 4 bits

   As loaded: EQY PASS: every partition proved in 0.6 s.

2. Drop a partial product

   In gate.sv add && i != 2 to the if: UNKNOWN: equivalence not proven. The runner cannot show whether the failure is reachable; with no cut points inside this one partition, it is.

3. Grow it

   Set W to 6 in both files: EQY PASS: every partition proved in 0.6 s. Then try 9 and watch the budget.

Check Yourself

module mul(input [3:0] a, b, output [7:0] p);
  assign p = a * b;
endmodule

module mul(input [3:0] a, b, output reg [7:0] p);
  integer i;
  always @* begin   // the shift-add multiplier of F2.2, unrolled: one partial product per bit of b
    p = 0;
    for (i = 0; i < 4; i = i + 1)
      if (b[i]) p = p + ({4'd0, a} << i);
  end
endmodule