Lesson 6.4 · FPV for Bug Hunting and Signoff

End-to-end data checking with a tracked item

How do we check "data leaves in the order it entered" without writing a full reference model of the FIFO? The trick is to let the formal tool choose one arbitrary push and follow only that entry:

A free input trk_arm lets the tool decide which push to track.
When that push happens, record its data and how many entries are ahead of it.
Every pop decrements the "ahead" counter. When it reaches zero, the next pop must return the recorded data.

Because the tool explores every possible choice of trk_arm, proving the check for "one arbitrary item" proves it for every item — at the cost of a few extra flops instead of a full model.

The tool tracks one arbitrary entry (T). It only needs to count how many entries are in front of it.

sync_fifo_fv.sv

// sync_fifo_fv.sv — signoff wrapper with tracked-item data check
module sync_fifo_fv #(
  parameter int WIDTH = 2,
  parameter int DEPTH = 4
) (
  input logic             clk,
  input logic             rst,
  input logic             push,
  input logic [WIDTH-1:0] wdata,
  input logic             pop,
  input logic             trk_arm      // free: which push to track
);
  localparam int CW = $clog2(DEPTH + 1);

  logic [WIDTH-1:0] rdata;
  logic             full, empty;
  logic [CW-1:0]    count;

  sync_fifo #(.WIDTH(WIDTH), .DEPTH(DEPTH)) dut (.*);

  initial assume (rst);
  default clocking cb @(posedge clk); endclocking
  default disable iff (rst);

  wire do_push = push && !full;
  wire do_pop  = pop  && !empty;

  // ---------------------------------------------------- tracked-item model
  logic             tracking;   // tracked entry is inside the FIFO
  logic [WIDTH-1:0] trk_data;   // its value
  logic [CW-1:0]    ahead;      // entries in front of it

  always_ff @(posedge clk) begin
    if (rst) begin
      tracking <= 1'b0;
      trk_data <= '0;
      ahead    <= '0;
    end else if (!tracking) begin
      if (do_push && trk_arm) begin
        tracking <= 1'b1;
        trk_data <= wdata;
        ahead    <= count - CW'(do_pop);         // a same-cycle pop removes one in front
      end
    end else if (do_pop) begin
      if (ahead == '0) tracking <= 1'b0;          // tracked entry leaves now
      else             ahead    <= ahead - 1'b1;
    end
  end

  // ---------------------------------------------------- data integrity
  a_data_order: assert property (tracking && do_pop && ahead == '0 |-> rdata == trk_data);
  a_ahead_ok:   assert property (tracking |-> ahead < count);         // helper invariant

  // ---------------------------------------------------- count / flags
  a_count_range: assert property (count <= CW'(DEPTH));
  a_flags:       assert property (full == (count == CW'(DEPTH)) && empty == (count == '0));
  a_count_inc:   assert property (do_push && !do_pop |=> count == $past(count) + 1'b1);
  a_count_dec:   assert property (!do_push && do_pop |=> count == $past(count) - 1'b1);
  a_count_hold:  assert property (do_push == do_pop  |=> count == $past(count));
  a_full_drop:   assert property (full && push && !pop |=> full && $stable(rdata));
  a_empty_pop:   assert property (empty && pop && !push |=> empty);

  // ---------------------------------------------------- covers
  c_full:            cover property (full);
  c_full_then_empty: cover property (full ##[1:$] empty);
  c_push_pop_full:   cover property (full && push && pop);
  c_track_deep:      cover property (tracking && ahead == CW'(DEPTH - 1));
  c_track_out:       cover property (tracking && do_pop && ahead == '0);
endmodule

sync_fifo.sby

# sync_fifo.sby
[tasks]
prove
cover

[options]
prove: mode prove
cover: mode cover
depth 16

[engines]
prove: abc pdr
cover: smtbmc

[script]
read -formal sync_fifo.sv sync_fifo_fv.sv
prep -top sync_fifo_fv

[files]
sync_fifo.sv
sync_fifo_fv.sv