Engine Choice and Run Management

One Question, One First Engine

Bugs come out of bmc: it is complete up to its depth and each step is a plain satisfiability query. Proofs need prove: k-induction is quick when the property is inductive, PDR when it is not. Wide arithmetic favours word-level SMT; long control favours bit-level PDR.

The Spine Under Five Engines

Every SMT solver ends without a proof; PDR proves the same properties in 1.8 s with no invariant written by hand, because it builds its own (F2.5). With F4.6’s invariants, k-induction closes it too.

Measured: A Different Winner Each Time

The control proof is not inductive, so every SMT solver stops at UNKNOWN and PDR proves it. The 6-bit multiplier proof is the reverse: induction closes it and PDR runs out of time. On the 8-bit bounded check the slowest SMT solver takes 2.8 times as long as the fastest.

The shallow bug is found by every engine within a second; PDR’s trace is one step longer (12 against 11). For bugs, the depth matters more than the engine.

Several Engines in One Task

[options]
mode prove
depth 12
timeout 60

[engines]
smtbmc yices
abc pdr

[script]
read_verilog -formal -sv design.sv
prep -top fifo16

[files]
design.sv

engine_0 (smtbmc yices) returned pass for basecase
engine_0 (smtbmc yices) returned FAIL for induction
  failed assertion fifo16._witness_.check_design_sv_20_assert_30 at design.sv:20.16-20.40
engine_1 (abc pdr) returned PASS
engine_1 did not produce any traces
DONE (PASS, rc=0)

engine_0 (smtbmc yices) returned FAIL for induction
  failed assertion fifo4sb._witness_.check_design_sv_40_assert_50 at design.sv:40.24-40.44
engine_1 (abc pdr) returned PASS
engine_1 did not produce any traces
engine_2 (smtbmc bitwuzla) did not return a status
  failed assertion fifo4sb._witness_.check_design_sv_40_assert_50 at design.sv:40.24-40.44
DONE (PASS, rc=0)

An UNKNOWN from one engine does not end the task; a definite answer from any engine does. timeout ends a run on purpose and reports TIMEOUT, which claims nothing. expect names the status you want, so a regression fails loudly when it changes.

[tasks] splits one file into separate jobs, one per property group or engine, each with its own timeout and expect. The site’s 20-second budget is such a timeout line. A TIMEOUT from bmc asks for the depth argument (F4.1) or an abstraction; one from PDR asks for asserted invariants (F4.6) or a decomposition (F4.3).

What Each Status Lets You Claim

A sign-off table lists the engine, the status and the depth for every property. A TIMEOUT in it is an open item, never a pass.

Asked in Interviews

Try It

The lab is fifo16 from F2.4 under abc pdr. Measured: Prove PASS, 1.4 s.

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

1. Swap the engine

   Run the same design with smtbmc yices in prove mode at depth 12 and read the verdict.

2. Swap the design

   Paste the 6-bit multiplier from F2.2 and run it under smtbmc bitwuzla, prove depth 10, then under abc pdr.

3. Hunt the bug

   Make the multiplier test the wrong bit and run bmc at depth 14 with two different solvers. Compare the reported steps.

Check Yourself

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);
  end
endmodule

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