SAT and SMT in One Lesson

One Question

A SAT solver answers one question: is there a 0/1 assignment that makes every clause true? SAT means yes, and here it is: the model. UNSAT means no such assignment exists.

Modern solvers (CDCL) decide, propagate, hit a conflict, learn a clause that forbids it, and jump back. DPLL (1962) had the decide-propagate-backtrack loop; GRASP (1999) added clause learning; Chaff (2001) made propagation cheap.

Every BMC Query Is This Question

Checking assumptions in step 0..
Checking assertions in step 0..
Checking assumptions in step 1..
Checking assertions in step 1..
Checking assumptions in step 2..
Checking assertions in step 2..
Checking assumptions in step 3..
Checking assertions in step 3..
Checking assumptions in step 4..
Checking assertions in step 4..
BMC failed!
Assert failed in seq3: design.sv:12.35-12.47 (_witness_.check_design_sv_12_assert_16)
Status: failed

Each query asks: is there an input sequence of length k that reaches a bad state? A satisfiable answer is a counterexample, and its model is the trace. An unsatisfiable answer says no failure exists at that step. In formal, UNSAT is the good news.

Words and Gates

An SMT solver is SAT plus theories. The bit-vector theory knows that a + b is an addition, rewrites x + 0 to x, and turns words into gates only when it must. smtbmc writes SMT-LIB2 with bit-vectors and arrays; abc works on the AIGER, where everything is already gates.

Multiplication is hard for every engine: here each extra bit multiplies the time by two to eight. The four SMT solvers differ in rewriting and in their SAT core, by design. On control logic a bit-level engine often wins; F4.7 measures that habit across engines.

Same Verdict, Different Time

assert property (@(posedge clk) disable iff (rst)
  done |-> p == a_q * b_q);

  reg [5:0] a_q=0, b_q=0;
  always @(posedge clk) if (!rst && start && !busy) begin a_q <= a; b_q <= b; end
  always @(posedge clk) if (!rst && done) assert(p == a_q * b_q);

Asked in Interviews

Try It

The lab runs the 6-bit multiplier in bmc mode at depth 10 with smtbmc yices. Measured: PASS in 0.8 s.

1. Change the solver

   Switch the engine to Boolector, Bitwuzla and Z3 in turn. The verdict stays; read the times.

2. Plant the bug

   Change mplier[0] to mplier[1] and run two solvers. Both report the same step.

3. Count the queries

   Open the SBY log: one "Checking assertions in step" line per step, each one a solver call.

Check Yourself

module mul_sa(input clk, rst, start, input [5:0] a, b,
  output reg done=0, output reg [11:0] p=0);
  reg [11:0] mcand=0;
  reg [5:0] mplier=0;
  reg [2:0] n=0;
  reg busy=0;
  always @(posedge clk) begin
    done <= 0;
    if (rst) begin busy <= 0; p <= 0; n <= 0; end
    else if (start && !busy) begin
      busy <= 1; p <= 0; mcand <= a; mplier <= b; n <= 3'd6;
    end else if (busy) begin
      if (mplier[1]) p <= p + mcand;   // bug: wrong bit
      mcand <= mcand << 1;
      mplier <= mplier >> 1;
      n <= n - 3'd1;
      if (n == 3'd1) begin busy <= 0; done <= 1; end
    end
  end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // Modelling flops: the operands captured at start
  reg [5:0] a_q=0, b_q=0;
  always @(posedge clk) if (!rst && start && !busy) begin a_q <= a; b_q <= b; end
  always @(posedge clk) if (!rst && done) assert(p == a_q * b_q);
endmodule