From RTL to a Transition System

The Box Every Prover Sees

A prover does not see modules, processes or a clock. It sees state bits (the flops), inputs nobody drives, one function that computes the next state, the allowed first states and the bad states. That object is a transition system.

assert property (@(posedge clk) disable iff (rst)
  t1 |-> $past(t0) || $past(t1));

  // t1 |-> $past(t0) || $past(t1), with its history kept in flops
  reg f_past_valid=0, t0_q=0, t1_q=0;
  always @(posedge clk) begin
    f_past_valid <= 1; t0_q <= t0; t1_q <= t1;
    if (f_past_valid && !rst && t1) assert(t0_q || t1_q);
  end

From design.sv to a Solver File

Each engine reads its own file. smtbmc reads SMT-LIB2, where a 4-bit add stays one operation. ABC and the aiger engines read AIGER, where everything is AND gates, inverters and latches. btormc and pono read BTOR2, which keeps words like SMT-LIB2.

[options]
mode bmc
depth 5

[engines]
smtbmc yices
abc bmc3
btor btormc

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

[files]
design.sv

Read the AIGER Header

aag 33 3 8 0 22 1 3 0 0
input 0 0 clk
input 1 0 rst
input 2 0 en
latch 0 0 t0
latch 1 0 t1
latch 2 0 f_past_valid
latch 3 0 t0_q
latch 4 0 t1_q

I counts clk, but every latch now steps once per frame, so the clock drives nothing. C counts the two reset assumptions and one more that the flow adds to pin clk.

Words and Bits

30 sort bitvec 4
31 const 30 0000
32 state 30 a
33 init 30 32 31
43 uext 30 6 3
44 add 30 32 43
45 ite 30 3 44 32
46 ite 30 4 31 45
47 next 30 32 46
17 bad 16 _witness_.check_design_sv_10_assert_11

BTOR2 and SMT-LIB2 keep a + 1 as one operation on a 4-bit word. AIGER has already turned it into gates. F2.2 shows why both exist: word-level solvers rewrite arithmetic, bit-level engines such as PDR need gates.

The .smt2 file has the box as named functions: tog2_i is the initial-state test, tog2_t the transition, tog2_a the assertions and tog2_u the assumptions.

Add a Flop Nobody Reads

The new flop t2 feeds no assertion, so it is outside the cone of influence: the state and inputs a property can depend on. The AIGER flow optimized it away. The other two models keep it and leave the pruning to the solver. F4.2 uses this rule to shrink real proofs.

Asked in Interviews

Try It

The lab runs tog2 in bmc mode at depth 5 with smtbmc yices. Measured: PASS, 500 ms on this machine.

1. Run it

   Read the verdict and the SBY summary. A bounded PASS at depth 5 covers samples 0 to 3.

2. Add a third flop

   Rename the module and top to tog3, add t2 that toggles when t0 && t1 && en, and re-run. The verdict does not change: no assertion reads t2.

3. Break the cone

   Delete if (t0) so t1 toggles on en alone, and re-run. The solver now reaches a bad state; read the step it reports.

Check Yourself

module tog2(input clk, rst, en, output reg t0=0, output reg t1=0);
  always @(posedge clk)
    if (rst) begin t0 <= 0; t1 <= 0; end
    else if (en) begin
      t0 <= !t0;
      t1 <= !t1;          // bug: toggles without t0
    end
  always @(posedge clk) begin
    if ($initstate) begin assume(rst); end else begin assume(!rst); end
  end
  // t1 |-> $past(t0) || $past(t1), with its history kept in flops
  reg f_past_valid=0, t0_q=0, t1_q=0;
  always @(posedge clk) begin
    f_past_valid <= 1; t0_q <= t0; t1_q <= t1;
    if (f_past_valid && !rst && t1) assert(t0_q || t1_q);
  end
endmodule