FIFO Assertions

What a FIFO checker must prove

A FIFO has four failure modes that escape casual testing: overflow (push when full silently drops or corrupts data), underflow (pop when empty returns garbage), bookkeeping drift (count, pointers, and flags disagree — works for a while, fails at wrap), and data corruption (right occupancy, wrong bytes). A complete checker covers all four with independent rules, so a failure message tells you which mechanism broke rather than just “data mismatched eventually.”

DEPTH=4 FIFO life cycle — count/flag consistency at every tick

  tick   :   1    2    3    4    5    6    7    8    9
  push   :   1    1    1    1    0    0    0    0    0
  pop    :   0    0    0    0    1    1    1    1    1
  count  :   0    1    2    3    4    3    2    1    0   (sampled)
  empty  :   1    0    0    0    0    0    0    0    1
  full   :   0    0    0    0    1    0    0    0    0
                                 ^                   ^
            full==(count==4) ────┘                   └── empty==(count==0)
  tick 9: pop with count==1 legal; a pop at tick 10 (count 0) = underflow

The canonical ruleset

1. No overflow: never push (without simultaneous pop) while full.

2. No underflow: never pop while empty.

3. Count consistency: count changes by exactly the push/pop delta each cycle.

4. Pointer consistency: count equals wr_ptr − rd_ptr in modular arithmetic.

5. Flag consistency: empty ⇔ count==0, full ⇔ count==DEPTH; never both (unless DEPTH==0).

6. Data integrity: popped data equals the matching pushed data (preview of local variables).

Complete checker module

module fifo_checker #(
  parameter int DEPTH = 16,
  parameter int PTR_W = $clog2(DEPTH)
)(
  input logic             clk, rst_n,
  input logic             push, pop, full, empty,
  input logic [PTR_W:0]   count,            // one extra bit: 0..DEPTH
  input logic [PTR_W:0]   wr_ptr, rd_ptr    // free-running, extra MSB
);
  // R1/R2: interface legality (allow push+pop while full: net zero)
  a_no_overflow: assert property (@(posedge clk) disable iff (!rst_n)
    (push && !pop) |-> !full)
    else $error("push while full");
  a_no_underflow: assert property (@(posedge clk) disable iff (!rst_n)
    pop |-> !empty)
    else $error("pop while empty");

  // R3: count moves by exactly the push/pop delta
  a_count_delta: assert property (@(posedge clk) disable iff (!rst_n)
    ##1 count == $past(count) + (PTR_W+1)'($past(push && !full))
                              - (PTR_W+1)'($past(pop  && !empty)))
    else $error("count drifted from push/pop history");

  // R4: pointer math — free-running pointers, modular subtraction.
  // The extra MSB makes wr_ptr - rd_ptr equal occupancy directly.
  a_ptr_count: assert property (@(posedge clk) disable iff (!rst_n)
    count == (PTR_W+1)'(wr_ptr - rd_ptr))
    else $error("count vs pointer mismatch");

  // R5: flags derive from count; mutual exclusion for DEPTH>0
  a_empty_def: assert property (@(posedge clk) disable iff (!rst_n)
    empty == (count == 0));
  a_full_def:  assert property (@(posedge clk) disable iff (!rst_n)
    full  == (count == DEPTH));
  a_excl: assert property (@(posedge clk) disable iff (!rst_n)
    !(empty && full));   // holds because DEPTH > 0

  c_wrap: cover property (@(posedge clk)   // pointers wrapped past max
    $past(wr_ptr[PTR_W-1:0]) == DEPTH-1 && wr_ptr[PTR_W-1:0] == 0);
  c_full_to_empty: cover property (@(posedge clk)
    full ##[1:$] empty);                    // full drained completely
endmodule

Why the extra pointer MSB (DEPTH=4, PTR_W=2, pointers 3 bits)

  after 5 pushes, 1 pop:
    wr_ptr = 3'b101 (5)   rd_ptr = 3'b001 (1)
    count  = 5 - 1 = 4    → full, correct
  without the MSB (2-bit pointers):
    wr_ptr = 2'b01 (1)    rd_ptr = 2'b01 (1)
    wr_ptr - rd_ptr = 0   → empty and full are indistinguishable!
  The MSB disambiguates "same index, one lap apart" — assert R4
  on the FULL extended pointers, never the truncated indexes.

Data integrity and the local-variable boundary

Bookkeeping rules prove the FIFO stores the right number of elements — not the right elements. From the sampled-value lessons: when occupancy at pop time is a known constant K, rd_data == $past(wr_data, K, push) works, and a generate loop over K covers each occupancy. The general in-order check — any occupancy, simultaneous push+pop — wants a local variable that captures wr_data at push and waits for the matching pop. Preview:

// Per-occupancy form (from the sampled-values lesson):
generate for (genvar k = 1; k <= DEPTH; k++) begin : g_int
  assert property (@(posedge clk) disable iff (!rst_n)
    (pop && count == k) |-> rd_data == $past(wr_data, k, push));
end endgenerate

// Local-variable form (full treatment in the local-variables lesson):
// capture the data and ITS sequence number at push; check at the pop
// with the matching sequence number.
property p_fifo_data;
  logic [31:0] d;  int unsigned my_idx;
  @(posedge clk) disable iff (!rst_n)
    (push, d = wr_data, my_idx = push_cnt) |->
      first_match(##[1:$] (pop && pop_cnt == my_idx)) ##0
      (rd_data == d);
endproperty
a_data: assert property (p_fifo_data);

The local-variable form needs auxiliary modeling code (push_cnt/pop_cnt beat counters) — and that is normal: industrial checkers routinely pair a little modeling RTL with the assertions. Pure-SVA purity is not a goal; clarity and coverage are.

Async FIFOs and interview angle

Gray-pointer note for async FIFOs

In a dual-clock FIFO the pointers cross domains, and binary pointers can be sampled mid-transition with multiple bits changing — yielding a wildly wrong value. Hence Gray-coded pointer crossings: adjacent values differ in exactly one bit, so a metastable sample is off by at most one position — conservatively stale, never corrupt. The assertion-side contribution is single-domain and checkable: prove the Gray property itself, $countones($past(gray_ptr) ^ gray_ptr) <= 1 in the pointer's own domain. Do not try to assert occupancy across the two clocks — cross-domain sampling in SVA is race-dependent (see the clock-and-gating lesson); flag consistency in each domain plus the Gray invariant is the right division of labor.

Interview angle

“What would you assert on a FIFO?” — enumerate the six rules by name before writing any code; the count is the score. Three follow-ups recur: the pointer-width trick (why pointers carry an extra MSB and why count == wr_ptr - rd_ptr needs it — the wrap ambiguity above), the simultaneous push+pop subtlety (legal even when full: net occupancy change is zero — your overflow rule must say push && !pop |-> !full), and the async variant (Gray pointers; assert one-bit-change per domain; never assert across clocks). The data-integrity question is a deliberate bridge: the interviewer wants to hear you reach for local variables once occupancy is dynamic.

Key takeaways

• Four independent failure modes — overflow, underflow, bookkeeping drift, data corruption — need independent rules.

• Assert count against free-running extra-MSB pointers; truncated indexes cannot distinguish full from empty.

• push && !pop |-> !full — simultaneous push+pop at full is legal in most designs.

• Data integrity: $past per fixed occupancy; local variables once occupancy is dynamic.

• Async FIFOs: assert the Gray one-bit-change invariant per domain; never assert across clocks.

Common pitfalls

• Asserting count == wr_ptr - rd_ptr on truncated pointers — passes until the first wrap, then chaos.

• Forbidding push while full outright — rejects the legal simultaneous push+pop case.

• Checking flags only at empty/full extremes — drift in the middle range goes unnoticed until wrap.

• Cross-domain occupancy assertions on an async FIFO — race-dependent results, no silicon meaning.

• Skipping the wrap cover point — a regression that never wraps the pointers proves almost nothing.