Every plan row traces to this spec. Each numbered behavior becomes at least one feature, and each silence becomes a logged question.
FIFO SPECIFICATION (v1.2)
Parameters
WIDTH : data width in bits (default 8, range 1-64)
DEPTH : number of entries (default 16, power of 2, >= 2)
Interface (all synchronous to clk, async active-low rst_n)
write side: in_valid (in) in_ready (out) in_data[WIDTH] (in)
read side: out_valid (out) out_ready (in) out_data[WIDTH] (out)
status: full (out) empty (out)
Behavior
1. A push occurs when in_valid && in_ready on a clk edge.
2. A pop occurs when out_valid && out_ready on a clk edge.
3. in_ready == !full; out_valid == !empty.
4. full asserts when count == DEPTH; empty when count == 0.
5. Data emerges in push order (strict FIFO), unmodified.
6. Push at full is ignored (in_ready low blocks the handshake).
7. Simultaneous push+pop is legal whenever both handshakes can
occur (0 < count < DEPTH). At full, in_ready is low: the pop
proceeds and an offered push is not taken until in_ready
rises (spec v1.2 clarification Q-003).
8. rst_n clears the FIFO to empty within 1 cycle; in-flight
data is discarded.Three ambiguities needed answers before any code. Guessing from RTL is not verification.
Q-003: push and pop in the same cycle at full, allowed? Answer (architect, spec updated to v1.2): no. in_ready stays !full, so the pop proceeds and the offered push is not taken that cycle; it must wait for in_ready. A push accepted at full is a bug, even when a pop fires.
Q-004: out_data validity when empty, defined? Answer: undefined when out_valid is low. Checkers must not compare it.
Q-005: behavior if rst_n asserts mid-handshake? Answer: transaction discarded, no partial state. Flags valid 1 cycle after deassert.
One spec sentence can hide several features. Rule 7 becomes two rows because each needs different stimulus and a different check.
F-01 Data integrity: every pushed word pops exactly once, unmodified, in push order.
F-02 full asserts exactly at count == DEPTH, deasserts on the next pop.
F-03 empty asserts exactly at count == 0, deasserts on the next push.
F-04 in_ready mirrors !full; out_valid mirrors !empty (combinational, same cycle).
F-05 Push at full is blocked: no data loss, no corruption, count unchanged.
F-06 Pop at empty is blocked: no spurious data, count unchanged.
F-07 Simultaneous push+pop at intermediate fill: count unchanged, order preserved.
F-08 Push offered with a pop at full: pop proceeds, push blocked (in_ready low) until a slot is free, per Q-003.
F-09 Reset mid-traffic: empty within 1 cycle, in-flight data discarded, clean restart.
F-10 Backpressure: sustained out_ready == 0 fills the FIFO, release drains in order.
F-11 Parameter sweep: behavior holds at DEPTH 2 (minimum) and WIDTH 1 (degenerate).
VERIFICATION PLAN — fifo v1.2
ID │ Feature │ Approach │ Coverage / Check │ Owner
─────┼─────────────────────┼───────────────────────┼─────────────────────────┼──────
F-01 │ data integrity, │ random, all tests │ scoreboard in-order │ SB
│ in-order │ │ compare; a_data_integ │
F-02 │ full @ count=DEPTH │ burst-fill directed │ a_full_def; │ SB
│ │ + random │ cp_count.full bin │
F-03 │ empty @ count=0 │ drain directed │ a_empty_def; │ SB
│ │ + random │ cp_count.empty bin │
F-04 │ ready/valid mirror │ assertion, always on │ a_ready_def, a_valid_def│ SB
F-05 │ push @ full blocked │ stress + error test │ a_no_push_full; │ RK
│ │ │ cp_backpressure bin │
F-06 │ pop @ empty blocked │ stress + error test │ a_no_pop_empty; │ RK
│ │ │ x_op_state empty bin │
F-07 │ push+pop mid-level │ random mixed-rate │ x_op_state.both_mid │ SB
F-08 │ push offered @ full │ directed corner test │ cp_offer_at_full bin; │ SB
│ with a pop │ │ a_no_push_full │
F-09 │ reset mid-traffic │ reset-storm test │ cp_reset_busy bin; │ RK
│ │ │ post-reset SB restart │
F-10 │ backpressure drain │ burst/drain scenario │ cp_backpressure bins │ SB
F-11 │ param corners │ regression configs │ DEPTH=2 + WIDTH=1 runs │ RK
Status column omitted here — all rows start "open".The corner inventory is the FIFO bug map. Boundaries, simultaneity, reset, wrap-around and backpressure find the bugs that flat randomness misses.
Exact boundaries: the cycle full asserts, the cycle empty asserts. Off-by-one errors live at count == DEPTH-1 versus DEPTH.
Simultaneous push and pop at empty+1 and at full-1 (F-07), and a push offered during a pop at full (F-08). Pointer-update ordering bugs live here.
Reset mid-traffic, mid-burst, and reset released directly into a push (F-09).
Wrap-around: pointers crossing DEPTH back to 0 repeatedly. Tests that push fewer than DEPTH total items never exercise it.
Sustained backpressure, then sudden drain at full rate (F-10).
Each case needs different stimulus and a different check. Mid-level: both handshakes happen and count holds. Full: only the pop happens and the offered push is blocked per Q-003. Each closes a different coverage bin.
Wrap-around, the full boundary and the almost-full bins. The pointers never crossed back to zero.