// 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