BDDs, Interpolation and the Engine Zoo

Meet the engines behind every formal tool, see why no single one wins, and run the same proof through several of them.

Lesson: F2.6
Time: 15 min
Runs on: SymbiYosys
Check: 4 questions

A review asked why the formal team ran three engines on every property, and whether that was waste. The lead pulled the week’s log: one property proven only by PDR, one only by induction with helpers. No engine had won twice in a row.

Binary Decision Diagrams

A == b for 2-bit Words, as a BDDRead left to right: test a1, then b1, then a0, then b0. The a0 test is shared by both paths, so it is drawn once.

Read the diagram as text

a1: first variable in the order
b1, after a1 = 0: only b1 = 0 continues
b1, after a1 = 1: only b1 = 1 continues
a0: shared by both paths
b0, after a0 = 0: only b0 = 0 continues
b0, after a0 = 1: only b0 = 1 continues
1: the words are equal

a1 → b1, after a1 = 0: 0
a1 → b1, after a1 = 1: 1
b1, after a1 = 0 → a0: 0
b1, after a1 = 1 → a0: 1
a0 → b0, after a0 = 0: 0
a0 → b0, after a0 = 1: 1
b0, after a0 = 0 → 1: 0
b0, after a0 = 1 → 1: 1

Every edge not drawn goes to the 0 terminal (a mismatch). 8 nodes counting both terminals; with this interleaved order the BDD grows by three nodes per bit.

Before SAT, symbolic model checking stored sets of states as BDDs (Bryant, 1986): a decision graph with a fixed variable order and every repeated subgraph merged. Reachability is a fixed point of image computations on BDDs (Burch, Clarke, McMillan, Dill, Hwang, 1990).

Bits per word	a == b, interleaved order	a == b, all a then all b	Middle product bit, interleaved	Middle product bit, all a then all b
2	8	11	9	9
4	14	47	71	55
6	20	191	571	395
8	26	767	5271	2795

Exact node counts, terminals included, computed from the truth tables. Bryant (1991) proved that the middle bit of a product grows exponentially under every order.

The order decides everything, and a good one is hard to find. SAT-based BMC (Biere, 1999) removed the need to store state sets at all. Induction, interpolation and IC3 then brought unbounded proofs back on SAT.

Interpolation

An Interpolant on the Unrolled StripAn UNSAT BMC query is cut after the first step. The proof of UNSAT yields a formula over the step-1 state alone.

Read the diagram as text

Part A: initial state and the first step
Interpolant P(s1): implied by A, inconsistent with B
Part B: k − 1 more steps and a bad state
A and B: UNSAT: no counterexample of length k

Part A → Interpolant P(s1): implies
Interpolant P(s1) → Part B: contradicts
A and B: UNSAT → Interpolant P(s1): extracted from the proof

P over-approximates the states one step from reset that still cannot fail. Use P as the new initial set and repeat; when nothing new is added, the union is an invariant. Drawn, not measured.

Interpolation (McMillan, 2003) takes an unsatisfiable BMC query, splits it after the first transition, and reads a formula over the step-1 state out of the solver’s proof. Iterating it reaches a fixed point: a proof with no helpers. AVY (Vizel and Gurfinkel, 2014) combines it with PDR.

The Engine Zoo

Engine line	Algorithm	Model	Good for
`smtbmc <solver>`	BMC, k-induction, cover	SMT-LIB2, words	bugs, cover traces, induction with helpers
`abc bmc3`	BMC	AIGER, bits	deep bug hunting on control logic
`abc pdr`	IC3/PDR	AIGER, bits	proofs without helpers
`aiger rIC3`	a portfolio: IC3, k-induction, BMC	AIGER, bits	several algorithms in one call
`aiger avy`	interpolation plus PDR	AIGER, bits	proofs; see the race below
`aiger suprove`	liveness	AIGER, bits	F3.7

Engines in the pinned suite. The lab exposes the SMT solvers and abc pdr; the rest ran with SBY directly.

Commercial tools run a portfolio of such engines in parallel and report the first answer. Theorem proving (Coq, Isabelle, ACL2) is another discipline: a person writes the proof and the tool checks it. This track does not teach it.

One Race, Three Designs

Design	`smtbmc yices` (prove)	`abc pdr`	`aiger rIC3`	`aiger avy`
fifo16, no helpers	UNKNOWN, 0.6 s	PASS, 1.2 s	PASS, 0.5 s	TIMEOUT (30 s), no verdict, –
fifo16, two helpers	PASS, 0.5 s	PASS, 0.8 s	PASS, 0.2 s	ERROR, no verdict, –
mul_sa, W = 6	PASS, 0.8 s	PASS, 22.7 s	PASS, 1.3 s	TIMEOUT (30 s), no verdict, –

Measured. smtbmc used depth 12, 2 and 10. The mul_sa PDR and every rIC3 and AVY run used SBY directly with a 30 s limit; through the lab runner, mul_sa under PDR hit its 20 s limit.

Look down each column. Induction proves mul_sa at depth 10 (depth 9: UNKNOWN) but needs helpers for the FIFO. PDR proves the FIFO alone but takes 22.7 s on the multiplier. AVY ended in ERROR on the three-assertion FIFO and found nothing in 30 s on the other two. rIC3, itself a portfolio, answered all three within 1.3 s.

Measured SBY summary with two lines under [engines]: both start, the first answer wins, the other is stopped.

summary: engine_0 (smtbmc yices) returned pass for basecase
summary: engine_0 (smtbmc yices) returned pass for induction
summary: engine_0 did not produce any traces
summary: engine_1 (abc pdr) did not return a status
summary: engine_1 did not produce any traces
DONE (PASS, rc=0)

Asked in Interviews

Question	Answer
What were BDDs and why did SAT replace them for big designs?	Canonical ordered decision graphs for sets of states. Their size depends on the variable order and explodes on arithmetic; SAT-based methods never store state sets.
What is interpolation, in one sentence?	A formula over the shared variables, implied by the first part of an UNSAT formula and inconsistent with the rest, used to over-approximate the reachable states.
Why do commercial tools run several engines at once?	No engine dominates; the winner depends on the design and the property. Running a portfolio is the cheap way to find out.

Try It

The lab runs fifo16 with its helpers in prove mode, depth 2, under smtbmc yices. Measured: PASS in 0.5 s.

Swap engines
Run the same design under abc pdr and compare the times and the engine named in the summary.
Swap designs
Paste the F2.2 multiplier at W = 6. Run prove with smtbmc yices at depth 9, then 10. Then try abc pdr and read what the time limit does to the verdict.
Fill the table
Write down a winner per design. Before you knew the result, which engine would you have picked? F4.7 turns this into a habit: run them all.

Top moduleModeDepthEngine

design.sv

props.sv

Use assert property (@(posedge clk) ...);. Leave blank for immediate assertions in the design.

Inputs are free unless constrained. Run to find a counterexample or check a proof.

Model: one positive-edge clock, binary data. Sampled history requires declaration-initialized variables; primary-input history is unsupported.

SBY summary and log

Enable JavaScript to edit and run. The original design and properties follow.

module fifo16(input clk, rst, wr, rd, input [7:0] wdata,
  output [7:0] rdata, output empty, full);
  reg [7:0] mem [0:15];
  reg [4:0] wr_ptr=0, rd_ptr=0, count=0;
  assign empty = count == 5'd0;
  assign full  = count == 5'd16;
  wire do_wr = wr && !full, do_rd = rd && !empty;
  assign rdata = mem[rd_ptr[3:0]];
  always @(posedge clk)
    if (rst) begin wr_ptr <= 0; rd_ptr <= 0; count <= 0; end
    else begin
      if (do_wr) begin mem[wr_ptr[3:0]] <= wdata; wr_ptr <= wr_ptr + 5'd1; end
      if (do_rd) rd_ptr <= rd_ptr + 5'd1;
      count <= count + do_wr - do_rd;
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  always @(posedge clk) if (!rst) begin
    if (empty) assert(wr_ptr == rd_ptr);
    assert(count == wr_ptr - rd_ptr);   // helper 1
    assert(count <= 5'd16);             // helper 2
  end
endmodule

Check Yourself

Predict the outputmul_sa at W = 6, correct design, mode prove, depth 10, smtbmc yices, reset assumed in step 0. The verdict is:

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[0]) p <= p + mcand;
      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

ConceptWhich claim about BDDs is wrong?

A BDD’s size does not depend on the variable order.Sets of states can be stored as BDDs.A BDD is a reduced, ordered decision graph.The middle bit of a product has an exponential BDD.

ConceptWhat is an interpolant?

The BDD of the transition relation, built under the best variable order that the tool could find.A formula over the shared variables, implied by one half of an UNSAT formula and inconsistent with the other.A helper invariant that the engineer writes by hand to make the property inductive at a small depth.The shortest counterexample the solver returned for the unrolled formula, at the first depth that was satisfiable.

ConceptIn the measured two-engine summary, which engine produced the verdict?

Both, in two summariesNeither: the engines conflictedsmtbmc yicesabc pdr

Remember

BDDs store state sets canonically, but their size depends on the variable order and explodes on multipliers.
Interpolation turns an UNSAT BMC proof into an over-approximation of the reachable states.
No engine wins everywhere: induction, PDR and portfolios each won something here.
SBY runs every listed engine and reports the first answer.

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.