sync_fifo·A single-clock first-in, first-out buffer.
Verification plan for sfifo in the target configuration BW=8, LGFLEN=4 (depth 16), OPT_ASYNC_READ=0, OPT_WRITE_ON_FULL=0, OPT_READ_ON_EMPTY=0. The DUT has a plain valid-style push/pop interface with no bus protocol, so no library agent applies. A custom single-clock agent drives i_reset, i_wr, i_data and i_rd. A passive monitor samples all inputs and outputs at each rising edge. A cycle-accurate reference model holds a SystemVerilog queue of up to 16 bytes. At every edge it decides acceptance from its own pre-edge state: write accepted = i_wr && !reset && fill<16; read accepted = i_rd && !reset && fill>0. Reset clears the queue. In the cycle after each edge, a scoreboard compares o_fill, o_empty and o_full exactly against the model, and compares o_data against queue.front() whenever the model is non-empty. o_data is not checked while empty, since the spec leaves it undefined. SVA assertions in a bound checker cover the status invariants and the hold-stable rules. Directed tests target the hard edges: full, empty, fill=1, fill=15, pointer wrap, simultaneous read/write at every boundary, and reset with data held or with inputs active. Constrained-random traffic with varied write/read densities then sweeps all fill levels and pointer phases.
1) Power-on/reset test. Hold i_reset for several cycles with i_wr, i_rd and i_data randomly toggling. Check that fill=0, empty=1 and full=0 after the first reset edge and that nothing is accepted. 2) Single-word test. Write one word into the empty FIFO and check that o_empty drops and o_data equals the word in the next cycle; this exercises the registered read path with FWFT. Hold the word several idle cycles to check o_data stability, then read it and check empty. 3) Fill-to-full test. Write 16 words with no reads and check fill 1..16, with full asserting only after the 16th write. Then attempt writes while full, with distinct marker data, for several cycles, with and without i_rd. Drain all 16 and check order and that no marker word appears. Drain past empty with extra reads, then write again and verify. 4) Walking-bit data test. Write 0x01,0x02,...,0x80, then 0xFE,0xFD,...,0x7F, plus 0x00, 0xFF, 0xAA and 0x55, so every o_data bit is seen at 0 and 1 in every storage slot. Repeat at 16 different pointer offsets by pre-cycling 0..15 words, so every bit of every memory location is covered. 5) Pointer-wrap test. Stream more than 100 words with fill held at 1, 2, 8 and 15 using simultaneous read/write, so the pointers wrap many times at each occupancy. 6) Simultaneous read/write boundary tests. Apply i_wr&&i_rd at fill=0, 1, 2, 8, 15 and 16, single-shot and back-to-back. At fill=1 this checks the new word appears next cycle (read/write same-address bypass). At fill=0 only the write is accepted. At fill=16 only the read is accepted and full stays high for that cycle. 7) Read-on-empty tests. Issue repeated i_rd while empty, including in the cycle immediately after the last word is drained. Then write and check data integrity. 8) Mid-stream reset tests. Assert reset at fill=1, 8, 15 and 16, during simultaneous read/write, and with i_wr/i_rd high in the reset cycle. Use reset pulses of 1 cycle and of several cycles. Then refill with new data and check that no pre-reset data ever appears, including stale words at the read pointer slot. 9) Constrained-random regression of 50+ seeds, about 5k cycles each. Mix weighted modes: write-heavy (wr 90%, rd 20%), read-heavy (wr 20%, rd 90%), balanced 50/50, bursty (long all-write then all-read runs), and full-hover/empty-hover modes that keep fill near 16 or 0. Fully random i_data, independent of i_wr, so i_data activity during i_wr=0 is ignored. Add rare random resets at 0.5%. The scoreboard and SVA run throughout, and coverage closure drives seed count.
The FIFO holds up to 2^LGFLEN words (16 with the target parameters). It accepts exactly 16 writes from empty before reporting full.
REQ-CAP-1How it's tested: Reference model counts accepted writes from empty; scoreboard checks o_full is low after writes 1..15 and high after write 16, and o_fill==16. Directed check: all 16 words are read back in order, so no slot is lost or aliased.
o_fill equals the number of words held: the number of accepted writes minus the number of accepted reads since reset.
How it's tested: Scoreboard compares o_fill against the model queue size every cycle. SVA checks that o_fill is never greater than 16 and that per-edge o_fill delta equals (wr_acc - rd_acc).
o_empty is high exactly when o_fill is 0.
How it's tested: SVA: o_empty == (o_fill==0) every cycle out of reset. Scoreboard compares o_empty against model.
o_full is high exactly when o_fill is 2^LGFLEN.
How it's tested: SVA: o_full == (o_fill==16) every cycle. Scoreboard compares o_full against model.
o_fill, o_empty and o_full change only on a clock edge: an accepted write or read at one edge is reflected in the status outputs for the following cycle, never earlier in the same cycle.
How it's tested: SVA, sampled with #1step and mid-cycle: o_fill, o_empty and o_full are stable between rising edges and do not change when i_wr/i_rd toggle mid-cycle. The monitor samples outputs just before each edge and checks they equal the post-previous-edge model value, not a value reflecting current-cycle inputs.
A write is accepted when i_wr is high and o_full is low at a rising clock edge. The word on i_data becomes the newest entry.
How it's tested: Reference model pushes i_data on accepted writes. Scoreboard verifies the word appears on o_data at the correct position in read-out order. Checks that i_data is ignored when i_wr is low, since random i_data toggles during idle never appear.
A write while the FIFO is full is ignored: no stored word changes, o_fill stays at 2^LGFLEN, and no data is lost or overwritten. This holds even when i_rd is high in the same cycle.
How it's tested: Model ignores the write when full. Scoreboard verifies fill stays 16 (no rd) and that the subsequent drain returns exactly the original 16 words. Marker data written during full never appears on o_data.
Whenever o_empty is low, o_data holds the oldest word in the FIFO (first-word fall-through). No read request is needed to see it.
How it's tested: Scoreboard compares o_data with model.front() every cycle that o_empty is low, not only on read cycles. SVA: o_data is stable while !o_empty and no read is accepted, even if writes occur. This catches the registered read path being updated by writes.
A read is accepted when i_rd is high and o_empty is low at a rising clock edge. The oldest word is removed and, if words remain, o_data shows the next oldest one in the following cycle.
How it's tested: Model pops on accepted reads. Scoreboard checks o_data equals the new front in the next cycle and that fill decrements.
A read while the FIFO is empty is ignored: o_fill stays at 0 and later data is not affected.
How it's tested: Model ignores the read. Scoreboard confirms fill=0 and empty stay asserted, with no underflow (o_fill never 31/wrap). The following written words read back correctly and in order.
Words are read out in exactly the order they were accepted. No word is lost, duplicated or corrupted, including when the internal storage wraps around after many writes.
REQ-ORD-1How it's tested: Scoreboard reference queue compares every read word in order. End-of-test check: model queue matches the DUT fill and all writes are accounted for (written = read + held + discarded by reset).
When the FIFO is neither empty nor full and both i_wr and i_rd are high, both are accepted at the same edge: the oldest word is removed, the new word is appended, and o_fill is unchanged.
How it's tested: Model performs pop and push. Scoreboard checks fill is unchanged, o_data advances to the next oldest, and the new word appears later in order.
When the FIFO holds exactly one word and both i_wr and i_rd are high, the held word is removed and the new word becomes the only entry. In the next cycle o_empty is low and o_data is the new word.
How it's tested: Scoreboard checks fill stays 1, o_empty stays low and o_data equals the new word in the next cycle. This targets the registered read path bypass, where the new word is written to the slot currently being read next.
When the FIFO is empty and both i_wr and i_rd are high, only the write is accepted (see REQ-RD-3).
How it's tested: Model accepts the write only. Scoreboard checks fill=1, o_empty low and o_data equals the written word next cycle (no pass-through and no lost word).
When the FIFO is full and both i_wr and i_rd are high, only the read is accepted (see REQ-WR-2); o_full stays high during that cycle.
How it's tested: Model accepts the read only, giving fill=15 next cycle. SVA checks o_full remains high within the cycle. Scoreboard checks the written word is discarded and never appears, and the oldest is removed.
While i_reset is high at a clock edge, the FIFO is emptied: in the next cycle o_fill is 0, o_empty is high and o_full is low. Writes and reads in a reset cycle are ignored.
How it's tested: Model clears on reset and ignores ops in that cycle. Scoreboard and SVA check that i_reset at edge N implies o_fill==0, o_empty and !o_full at N+1. A write in the reset cycle never appears on o_data.
Reset may be applied at any time, including when the FIFO holds data. After reset the FIFO behaves exactly like a freshly reset FIFO: words written afterwards are read back in order and no word from before the reset ever appears on o_data.
How it's tested: Scoreboard flushes the model on reset and tags pre-reset words. Any later o_data match to a pre-reset-only marker, or any mismatch versus the post-reset queue, is an error. Pre-reset and post-reset data use disjoint value ranges where feasible.
Implied: o_data is stable while non-empty and no read is accepted. It must not change on writes, idle cycles, or ignored ops (write on full).
REQ-IMPL-1How it's tested: SVA: !o_empty && !(i_rd) at edge N implies o_data at N+1 == o_data at N, given no reset. Cross-checked by the scoreboard front compare.