A bounded check finds the bug in six steps

A 4-entry FIFO controller keeps a count register beside its pointers. A bounded model check stops at step 6 with Assert failed in fifo_ctrl: a_count: push and pop arrived together three times in a row, and count reached 5 in a FIFO that holds 4.

This lesson runs the whole loop by hand with open-source tools: write the property, run the bounded check, read the counterexample, fix the RTL, then try to prove it for every cycle. The picture is the counterexample the tool produced.

Each column is one solver step, which is one clock cycle. Inputs in a step change the registers seen in the next step.

• Step 0: the assumption holds reset low, so every register is cleared.

• Step 1: push and pop together on an empty FIFO. The pop is refused, the push is accepted, so used and count are both 1 in step 2.

• Steps 3 to 5: push and pop are both accepted. used stays at 2, but count goes up by one each time.

• Step 6: count is 5, so a_count fails. The solver stops at the first failing step, so this is the shortest failing trace.

The design and its properties

The pointers carry a lap bit, so used = wptr - rptr is the true occupancy and decides full and empty. The count register is a second copy of the fill level for a status register, and the bug is in how it counts a push and a pop on the same edge.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

// Control half of a 4-entry FIFO: pointers decide full and empty,
// and a separate count register reports the fill level to software.
module fifo_ctrl (
  input  logic       clk, rst_n, push, pop,
  output logic       full, empty,
  output logic [2:0] count
);
  logic [2:0] wptr, rptr;                    // 2 address bits + 1 lap bit
  wire  [2:0] used  = wptr - rptr;           // true occupancy, 0 to 4
  assign full  = (used == 3'd4);
  assign empty = (used == 3'd0);
  wire wr_ok = push && !full;
  wire rd_ok = pop  && !empty;

  always_ff @(posedge clk)
    if (!rst_n) begin
      wptr <= '0; rptr <= '0; count <= '0;
    end else begin
      if (wr_ok) wptr <= wptr + 3'd1;
      if (rd_ok) rptr <= rptr + 3'd1;
      if (wr_ok)      count <= count + 3'd1;   // bug: push and pop together
      else if (rd_ok) count <= count - 3'd1;   //      count as a push only
    end

`ifdef FORMAL
  logic past_valid = 1'b0;
  always_ff @(posedge clk) past_valid <= 1'b1;
  always @(*) if (!past_valid) assume (!rst_n);       // start in reset
  always @(*) if (past_valid) a_count: assert (count <= 3'd4);
`endif
endmodule

• `past_valid` is 0 only in the first cycle. It is a formal-only register with an initial value, which the solver treats as the start state.

• The assume is the only input constraint: the run starts in reset. Every later push and pop value is free, so the solver tries all of them.

• The assert is an immediate assertion checked in every cycle after the first. a_count names it in the tool output.

• read_verilog -formal defines FORMAL, so simulation and synthesis never see this block.

Run the bounded check

Yosys turns the design into a model the solver can read; yosys-smtbmc then unrolls it for 20 cycles from reset and asks z3 for any input sequence that breaks an assertion. async2sync is needed even with a synchronous reset: write_smt2 refuses the assertion cells until it, or clk2fflogic, has lowered them.

$ yosys -q -p "read_verilog -formal -sv fifo_ctrl.sv; prep -top fifo_ctrl; async2sync; write_smt2 -wires fifo_ctrl.smt2"
$ yosys-smtbmc -s z3 -t 20 --dump-vcd cex.vcd fifo_ctrl.smt2
##   0:00:00  Solver: z3
##   0:00:00  Checking assertions in step 0..
##   0:00:00  Checking assertions in step 1..
...
##   0:00:00  Checking assertions in step 6..
##   0:00:00  BMC failed!
##   0:00:00  Assert failed in fifo_ctrl: a_count
##   0:00:00  Writing trace to VCD file: cex.vcd
##   0:00:00  Status: FAILED

cex.vcd holds every signal for every step; the figure above is drawn from it. Read a counterexample the way you read a failing simulation: find the step where the assertion fails, then walk back to the first step where the design did something you did not intend. Here that is step 3, where both operations are accepted and only count moves.

Fix it, and the bounded check passes

1
2
3
4
5
6

// snippet: the count update in fifo_ctrl after the fix
      case ({wr_ok, rd_ok})                    // fix: both together leave it alone
        2'b10:   count <= count + 3'd1;
        2'b01:   count <= count - 3'd1;
        default: count <= count;
      endcase

$ yosys-smtbmc -s z3 -t 20 fifo_ctrl.smt2
##   0:00:00  Solver: z3
##   0:00:00  Checking assertions in step 0..
...
##   0:00:07  Checking assertions in step 19..
##   0:00:11  Status: PASSED

This says no input sequence breaks a_count in the first 20 cycles after reset. It says nothing about cycle 21, as What formal adds beyond simulation explains. A 4-entry FIFO probably shows every behaviour within 20 cycles, but "probably" is not a proof.

Induction: from a bounded pass to a proof

Induction asks a different question. Take any state, reachable or not, in which the assertions held for 20 steps in a row; can the next step break one? If not, no run from reset can ever break them. The -i flag runs that check.

$ yosys-smtbmc -s z3 -i -t 20 --dump-vcd ind.vcd fifo_ctrl.smt2
##   0:00:00  Solver: z3
##   0:00:00  Trying induction in step 20..
##   0:00:00  Trying induction in step 19..
...
##   0:00:00  Trying induction in step 0..
##   0:00:00  Temporal induction failed!
##   0:00:00  Assert failed in fifo_ctrl: a_count
##   0:00:00  Writing trace to VCD file: ind.vcd
##   0:00:00  Status: FAILED

The fixed design fails induction. The trace in ind.vcd does not start from reset:

No run from reset reaches step 0 of this trace, because count and used start equal and the fixed RTL moves them together. But a_count only says count <= 4, and count = 1 with used = 2 satisfies it, so induction may start there. A deeper induction does not help: a count one behind stays one behind for ever.

The cure is a helper invariant: an extra assertion that rules out the unreachable states. It is proved together with a_count.

// snippet: one more line in the FORMAL block
  always @(*) if (past_valid) a_match: assert (count == used);   // helper invariant

$ yosys-smtbmc -s z3 -i -t 20 fifo_ctrl.smt2
##   0:00:00  Solver: z3
##   0:00:00  Trying induction in step 20..
##   0:00:00  Trying induction in step 19..
##   0:00:00  Temporal induction successful.
##   0:00:00  Status: PASSED

With both assertions, one step is enough: if count == used and count <= 4 hold now, the RTL keeps them true. Together with the passing bounded check from reset, a_count is now proved for every cycle, under the reset assumption.

Common mistakes

Testbench

A simulation replay of the counterexample on the fixed RTL: the same push and pop values for steps 1 to 5, then 2000 random cycles, checking count == wptr - rptr after every edge. On the buggy RTL the same replay ends with count at 5 and used at 2.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

`timescale 1ns/1ps
// The fixed fifo_ctrl, with the helper assertion in its FORMAL block.
module fifo_ctrl (
  input  logic       clk, rst_n, push, pop,
  output logic       full, empty,
  output logic [2:0] count
);
  logic [2:0] wptr, rptr;                    // 2 address bits + 1 lap bit
  wire  [2:0] used  = wptr - rptr;           // true occupancy, 0 to 4
  assign full  = (used == 3'd4);
  assign empty = (used == 3'd0);
  wire wr_ok = push && !full;
  wire rd_ok = pop  && !empty;

  always_ff @(posedge clk)
    if (!rst_n) begin
      wptr <= '0; rptr <= '0; count <= '0;
    end else begin
      if (wr_ok) wptr <= wptr + 3'd1;
      if (rd_ok) rptr <= rptr + 3'd1;
      case ({wr_ok, rd_ok})                    // fix: both together leave it alone
        2'b10:   count <= count + 3'd1;
        2'b01:   count <= count - 3'd1;
        default: count <= count;
      endcase
    end

`ifdef FORMAL
  logic past_valid = 1'b0;
  always_ff @(posedge clk) past_valid <= 1'b1;
  always @(*) if (!past_valid) assume (!rst_n);       // start in reset
  always @(*) if (past_valid) a_count: assert (count <= 3'd4);
  always @(*) if (past_valid) a_match: assert (count == used);   // helper invariant
`endif
endmodule

Related topics

• What formal adds beyond simulation

• Assumption discipline

• SVA cheat sheet and bug hunt