FIFO Ordering and Data Integrity

On this page

Part 5 of 10, lesson 15 of 20Formal ApplicationsAll levels

Why it matters

The FIFO counts correctly and delivers the wrong word. Control properties, occupancy within range, flags consistent, count the pushes and pops, all pass, because none of them looks at the bytes. The symptom is silent data corruption that only a data-integrity property catches: follow one symbolic slot from write to read and check it reads back what was written. That property needs the abstraction this lesson uses, because following every word through a 32-bit memory would drown the proof.

The core idea

Prove in layers. State properties pin the control: occupancy in range, flags matching count, pointers consistent with count. Transition properties check each push and pop moves the count by one, skipping the cycle after reset. Data integrity uses data independence: the FIFO never looks at the bytes, so following one free slot with one shadow value covers every slot and every word. The helper invariant says the tracked slot holds the shadow value while watched; without it the induction step starts from states where the memory disagrees, and no depth closes the proof.

What the layers prove together is order, but not each alone. The tracked-slot property says a word read from slot t equals the word written to slot t. FIFO order, the oldest word out first, comes from the pointer discipline: the write pointer advances by one per accepted push, the read pointer by one per accepted pop, and the count equals their difference (a_ptr, a_push_inc, a_pop_dec). A reorder bug would show up as a pointer bug. The set does not contain a mutant that reorders words, and the lesson does not claim one.

Property	Bug it kills	Shortest counterexample	Header depth
`a_range`, `a_flags`, `a_not_both`	fifth push into a full FIFO (BUG 1), pop of an empty FIFO wraps the count (BUG 2), full flag one entry early (BUG 3)	step 6, step 2, step 4	7, 3, 5
`a_ptr`, then `a_both`	push and pop together forget the pop (BUG 4)	step 3 (`a_ptr`)	4
`a_tracked`, `a_data`	bit 7 cleared on write (BUG 5): data corruption	step 2	3

Worked example: the combined proof

The full FIFO set proves with the helper: the base case holds from reset and the step holds for every pair of consecutive states satisfying the properties. Without the helper the bounded check still passes and the induction step fails: the second block runs depth 12 and the step still fails, and a sweep of every depth from 2 to 12 gave the same result. The helper is what makes the proof complete:

sync_fifo.sv

// formal: prove 4 expect pass slang top sync_fifo
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

sync_fifo.sv

// formal: prove 12 expect unproven slang top sync_fifo define HELPER=0
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

Now each class of bug. The fill bug is the lesson in choosing a bound: it needs four pushes to fill the FIFO and a fifth to overflow, so a bounded run to 6 passes and a run to 7 fails. The stimulus is reset at step 0, four pushes, and a fifth push at step 5 with the FIFO full, so the count reaches 5 at step 6:

sync_fifo.sv

// formal: bmc 6 expect pass slang top sync_fifo define BUG=1
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

sync_fifo.sv

// formal: bmc 7 expect fail slang top sync_fifo define BUG=1
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

sync_fifo.sv

// formal: bmc 3 expect fail slang top sync_fifo define BUG=2
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

Next, the early-full flag, the miscount, and the corruption. The miscount is caught by the internal pointer consistency at step 3, one step before the transition property would see it: the range property a_range never fails on this mutant within 12 steps, so only the pointer and transition checks see it. The corruption is invisible to every control property and is caught by the tracked data property at step 2. The early-full flag needs three pushes and is caught at step 4:

Steps	Stimulus	Mutant	Property	Outcome
1 to 3	push, then push and pop together	miscount	`a_ptr`	counterexample at step 3
1 to 2	push a word with bit 7 set, then read it	bit cleared	`a_data`	counterexample at step 2
1 to 4	three pushes	early full	`a_flags`	counterexample at step 4

sync_fifo.sv

// formal: bmc 4 expect fail slang top sync_fifo define BUG=4
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

sync_fifo.sv

// formal: bmc 3 expect fail slang top sync_fifo define BUG=5
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

With the a_ptr line deleted from the same module, the count-transition check a_both still finds the miscount, one step later:

sync_fifo.sv

// formal: bmc 4 expect pass slang top sync_fifo define BUG=4
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

sync_fifo.sv

// formal: bmc 5 expect fail slang top sync_fifo define BUG=4
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

sync_fifo.sv

// formal: bmc 5 expect fail slang top sync_fifo define BUG=3
`define FORMAL
module sync_fifo #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       push,
  input  wire [7:0] wdata,
  input  wire       pop,
  output wire [7:0] rdata,
  output wire       full,
  output wire       empty,
  output reg  [2:0] count
);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;

  assign full  = (BUG == 3) ? (count >= 3'd3) : (count == 3'd4);
  assign empty = (count == 3'd0);
  assign rdata = mem[rptr];

  wire do_push = push && (!full  || BUG == 1);
  wire do_pop  = pop  && (!empty || BUG == 2);

  always @(posedge clk) begin
    if (rst) begin
      wptr  <= 2'd0;
      rptr  <= 2'd0;
      count <= 3'd0;
    end else begin
      if (do_push) begin
        mem[wptr] <= (BUG == 5) ? {1'b0, wdata[6:0]} : wdata;
        wptr      <= wptr + 2'd1;
      end
      if (do_pop) rptr <= rptr + 2'd1;
      if (BUG == 4 && do_push && do_pop) count <= count + 3'd1;
      else                               count <= count + {2'b0, do_push} - {2'b0, do_pop};
    end
  end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);

  always @(*) if (!init) begin
    a_range:   assert (count <= 3'd4);
    a_flags:   assert (full == (count == 3'd4) && empty == (count == 3'd0));
    a_not_both: assert (!(full && empty));
    a_ptr:     assert (count[1:0] == (wptr - rptr));
  end

  always @(posedge clk) if (!init && !$past(rst)) begin
    a_push_inc: assert (!($past(push) && !$past(pop) && !$past(full)) || count == $past(count) + 3'd1);
    a_pop_dec:  assert (!($past(pop) && !$past(push) && !$past(empty)) || count == $past(count) - 3'd1);
    a_ovf_ign:  assert (!($past(push) && !$past(pop) && $past(count) == 3'd4) || count == $past(count));
    a_both:     assert (!($past(push) && $past(pop) && !$past(full) && !$past(empty)) || count == $past(count));
  end

  (* anyconst *) wire [1:0] tslot;
  reg [1:0] tslot_q;
  always @(posedge clk) tslot_q <= tslot;
  always @(*) if (!init) assume (tslot == tslot_q);
  reg       tv;
  reg [7:0] td;
  always @(posedge clk) begin
    if (rst) tv <= 1'b0;
    else begin
      if (do_push && wptr == tslot) begin tv <= 1'b1; td <= wdata; end
      else if (do_pop && rptr == tslot) tv <= 1'b0;
    end
  end
  always @(*) if (!init && tv && !empty && rptr == tslot) a_data: assert (rdata == td);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init && tv) a_tracked: assert (mem[tslot] == td);
  end endgenerate

  always @(*) if (!init) begin
    c_full:  cover (count == 3'd4);
    c_empty_after_use: cover (empty && tv == 1'b0 && wptr == 2'd2);
  end
  always @(posedge clk) if (!init) c_both: cover (push && pop && !full && !empty);
`endif
endmodule

What the review looks for

The set is complete: bounds, flags, transitions, slot integrity. A set without the tracked property is a control proof, not a data proof.
The helper is proved, never assumed, and the lesson states the induction behaviour with and without it, as the run above does.
Each bug class maps to the property that kills it, checked by mutation, not by assertion. No claim is made for a bug class that was not run.

Verify and debug

A control failure names the step and the count: check the push and pop enables first. A data failure names the tracked slot: the corruption sits between the push that loaded it and the pop that unloaded it. A proof that needs ever more depth is asking for the helper, not for patience. The abstraction behind the tracked slot, and why data independence justifies it, is taught in the property-development lessons.

Check yourself The data property passes without the helper at a large bound. Is the proof complete?

No: a bounded pass is bounded to that depth, and without the helper no induction closes, so longer runs may still fail. Add the tracked invariant and close the induction, or justify the bound from reset plus trigger plus latency.

Navigate

Why it matters

The core idea

Worked example: the combined proof

What the review looks for

Verify and debug

Related topics

FIFO Ordering and Data Integrity

Why it matters

The core idea

Worked example: the combined proof

What the review looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example: the combined proof

What the review looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example: the combined proof

What the review looks for

Verify and debug

Related topics

Up next