RTL Design Patterns · Chapter 7 · FIFO Design
Verifying a FIFO
A FIFO can simulate fine and still ship broken, corrupting one packet in ten thousand months later on real traffic. The reason engineers keep getting caught is that they confuse it simulated with it is verified. Running one scenario and eyeballing the result is a spot check. Verification is a claim that a reference model agreed with the design on every accepted operation, that the invariants held on every cycle, that each corner case was hit on purpose, and that constrained-random stimulus ran long enough to collide the boundary directed tests never time. This lesson builds the whole environment: a scoreboard that mirrors a golden queue, invariant assertions, a directed corner list, and a random driver with independent backpressure, in SystemVerilog, Verilog, and VHDL. The payoff is the bug only the scoreboard catches, a duplicated word on a simultaneous read and write at the wrap boundary.
Intermediate18 min readRTL Design PatternsFIFOVerificationScoreboardConstrained RandomAssertions
Chapter 7 · Section 7.6 · FIFO Design
1. The Engineering Problem
You are the verification owner for the packet FIFO from 7.1 — the circular buffer that decouples a burst parser from a slower checksum unit. The RTL author hands you a FIFO that already passed his bring-up test: a testbench that resets the FIFO, writes the eight values 0..7, reads eight values back, and prints PASS because the eight reads matched the eight writes in order. He is confident. The waveform is clean. Occupancy climbs to eight and drains to zero. By every appearance, the FIFO works.
It does not, and the reason it does not is the entire point of this page. His test drove exactly one trajectory through the state space: fill completely, then drain completely, with the write phase and the read phase never overlapping. It never wrote and read on the same cycle. It never let the FIFO hover near full while both sides were active. It never crossed the pointer-wrap boundary with a read and a write colliding on it. Those are precisely the cycles where a FIFO's subtle bugs live — a mis-handled simultaneous read+write, an off-by-one at the equal-pointer boundary of 7.2, a count that drifts by one under interleaved traffic. His test is not wrong; it is a spot check. It confirms the FIFO can do the one thing he asked and says nothing about the thousands of interleavings it cannot.
Your job is different from his. He asked "does it work?" and answered it with one run. You must answer "is it proven correct?" — and that is not a harder version of the same question, it is a different question with a different method. You cannot prove a sequential block correct by staring at a waveform, because the failure is one word in ten thousand on a timing your eye will never catch. You need a machine that checks every accepted operation against a known-good reference, that flags any violated invariant on any cycle, that hits each corner on purpose, and that runs long enough under randomized, adversarial traffic to stumble onto the collision the directed test skipped. That machine is a self-checking verification environment, and building it is what "verifying a FIFO" actually means.
// WHAT THE RTL AUTHOR RAN — a directed spot check. Fill, then drain. It PASSES,
// and it proves almost nothing about interleaved traffic.
// for (i=0;i<8;i=i+1) push(i); // write phase
// for (i=0;i<8;i=i+1) pop_check(i); // read phase — never overlaps the writes
// $display("PASS"); // one trajectory, eyeballed
// WHAT VERIFICATION MEANS — a REFERENCE-MODEL SCOREBOARD + INVARIANTS + CORNERS +
// CONSTRAINED-RANDOM, all passing. The scoreboard is a golden queue that mirrors
// every accepted push/pop and checks data + ORDER + no-loss + no-duplication;
// random rd/wr with independent backpressure eventually hits the collision the
// directed test never times, and the scoreboard names the exact failing cycle.
// (the environment this page builds — scoreboard, assertions, corners, random)2. Mental Model
Hold this model — a golden shadow queue, guardrail invariants, deliberate corners, and long random traffic, all judged by one scoreboard — and FIFO verification stops being guesswork. It is language-independent: the scoreboard, the invariants, the corners, and the random driver are the same environment in SystemVerilog, Verilog, and VHDL; only the queue syntax and the assertion idiom differ.
3. Pattern Anatomy
A FIFO verification environment is four cooperating parts wrapped around the DUT. Take them in turn.
The scoreboard — a reference-model queue (the oracle). The heart of the environment is a golden FIFO kept in software: a queue model_q. It is driven not by the requests (wr_en/rd_en) but by the DUT's accepted operations. On every cycle where a write is genuinely accepted (wr_en && !full), push wdata onto model_q (model_q.push_back(wdata)). On every cycle where a read is genuinely served (rd_en && !empty), pop the front (expected = model_q.pop_front()) and compare the DUT's rdata against it — accounting for the one-cycle registered-read latency, so you sample rdata the cycle after the read fires. Three failures collapse into that one comparison: a value mismatch is data corruption, a mismatch in the sequence of matches is reordering, and a queue that runs empty when the DUT still returns data (or holds words the DUT never returns) is duplication or loss. The scoreboard is the thing that turns all of these into a single, cycle-accurate rdata !== expected.
The invariant assertions — the always-true guardrails. Beside the scoreboard sit properties that must hold on every cycle regardless of data:
- Occupancy is bounded: the number of accepted-but-unread words is always in
0..DEPTH— never negative (underrun) and never aboveDEPTH(overrun). Equivalentlymodel_q.size()never exceedsDEPTH. - Never full and empty at once:
!(full && empty)always — the two flags are mutually exclusive except at the trivialDEPTH == 0case that does not exist. - Flags match occupancy:
emptyis true exactly when the model is empty;fullis true exactly when the model holdsDEPTHwords. This is where a 7.2 boundary bug shows up asfulldisagreeing withmodel_q.size() == DEPTH. - Accepted ops are legal: a write is only ever accepted when
!full; a read is only ever served when!empty.
The directed corner tests — the dangerous cycles, driven on purpose. The scoreboard is passive; it only judges cycles you actually drive. So the environment drives, deliberately, every corner where FIFOs break: fill-to-full (push DEPTH words, confirm full, confirm the next push is refused with no count change); drain-to-empty (pop everything, confirm empty, confirm the next pop is refused); simultaneous read+write on a partially-full FIFO (occupancy must stay equal — the both-at-once case); write-when-full rejected and read-when-empty rejected (the gates of 7.1); reset mid-operation (assert reset while data is in flight; both pointers and the occupancy clear, the FIFO reads empty, and the scoreboard flushes to match); and the pointer-wrap boundary (push/pop enough to roll a pointer past DEPTH-1, exercising the equal-pointer full/empty distinction of 7.2).
The constrained-random driver — long, adversarial, independent backpressure. Finally, a driver that randomizes wr_en and rd_en each cycle with independent probabilities — so writes and reads collide freely, including on the same cycle at the boundary — and runs for thousands of cycles, always feeding the same scoreboard and invariant checks. "Constrained" means the randomization respects the legal interface (you may still push when full; the FIFO must simply refuse, and the scoreboard models the refusal) and covers the corners with high probability. Independent backpressure is the load-bearing word: if reads and writes are correlated (always alternating, never overlapping) you reproduce the directed test and miss the collision; making them independent is what eventually schedules a read and a write on the exact cycle the wrap boundary is crossed.
FIFO verification environment — scoreboard + invariants + corners + constrained-random
data flowTwo anatomy details close the picture. First, the difference between "it works" and "it's proven" is structural, not effortful. A directed test and a scoreboard cost about the same to write; the scoreboard is not more work, it is a different architecture — a passive oracle that judges every cycle instead of an active script that checks one endpoint. Second, accepted-operation tracking is the subtlety that makes the scoreboard correct. You must push on wr_en && !full and pop on rd_en && !empty, not on the bare requests — because a write-when-full is refused by the DUT and must be refused by the model too, and a read-when-empty returns nothing. Model the requests and your golden queue drifts out of step with the hardware and the scoreboard reports false failures; model the accepted operations and it shadows the DUT exactly.
4. Real RTL Implementation
This is the core of the page, and here the "implementation" is the verification environment, not the FIFO — the DUT is the synchronous FIFO from 7.1/7.2. We build three pieces — (a) the reference-model scoreboard, (b) the invariant assertions, and (c) the directed corners plus a constrained-random driver with a self-checking PASS/FAIL summary — and each is shown in SystemVerilog, Verilog, and VHDL. The idea is identical in all three; only the queue mechanism and the assertion idiom differ, and seeing them side by side is what makes the methodology language-independent in your head.
Two disciplines run through every block. The scoreboard tracks accepted operations, never bare requests — push on wr_en && !full, pop on rd_en && !empty — or the golden queue drifts and every check becomes a false alarm. And the registered-read latency is honoured — the DUT of 7.1 delivers rdata one cycle after a read fires, so the scoreboard compares one cycle late. Miss either and you are debugging the testbench, not the FIFO.
4a. The reference-model scoreboard — the golden queue oracle
Start with the oracle. In SystemVerilog the golden queue is a native dynamic queue: logic [WIDTH-1:0] model_q [$] with push_back and pop_front. Sampled monitoring makes it clean — on each clock, observe whether a write and/or a read was accepted, mirror it into the queue, and on an accepted read compare rdata (one cycle later) against the popped expected. The two counters pushes and pops are a cheap cross-check that the FIFO neither dropped nor duplicated a word overall.
module fifo_scoreboard #(parameter int WIDTH = 8, DEPTH = 8) (
input logic clk, rst,
input logic wr_en, full, // write side of the DUT
input logic [WIDTH-1:0] wdata,
input logic rd_en, empty, // read side of the DUT
input logic [WIDTH-1:0] rdata
);
// The golden FIFO: a software queue that is correct BY CONSTRUCTION.
logic [WIDTH-1:0] model_q [$]; // reference queue
logic [WIDTH-1:0] expected;
int errors = 0, pushes = 0, pops = 0;
// A read accepted THIS cycle produces rdata NEXT cycle (registered read, 6.2),
// so remember that a read fired and check its data one cycle later.
logic rd_fired = 0;
always_ff @(posedge clk) begin
if (rst) begin
model_q.delete(); // flush the model on reset
rd_fired <= 1'b0;
end else begin
// 1) CHECK a read accepted on the PREVIOUS cycle: rdata is valid now.
if (rd_fired) begin
expected = model_q.pop_front(); // FIFO order oracle
pops++;
if (rdata !== expected) begin
$error("SCOREBOARD: rdata=%h expected=%h (order/dup/loss)", rdata, expected);
errors++;
end
end
// 2) MIRROR an ACCEPTED write into the model (never a bare wr_en).
if (wr_en && !full) begin
model_q.push_back(wdata); // q.push_back(wdata)
pushes++;
end
// 3) Remember whether a read is ACCEPTED this cycle (check it next cycle).
rd_fired <= (rd_en && !empty);
end
end
endmoduleThe whole oracle is those three steps: check the previously-fired read against the queue front, mirror the accepted write onto the queue's back, and latch whether a read fired for next cycle's check. Because model_q is a plain in-order queue, a reorder pops the wrong value, a duplicate makes the DUT return a word the queue has already popped, and a loss leaves a word in the queue the DUT never returns — all three surface as rdata !== expected at the exact failing cycle.
Verilog has no built-in queue, so the golden FIFO is an explicit array with head and tail indices — a software FIFO shadowing the hardware FIFO. q_push writes q[tail] and bumps tail; q_pop reads q[head] and bumps head; the occupancy is tail - head. Everything else is the same accepted-operation discipline.
// Reference-model scoreboard as Verilog tasks over an array queue with head/tail.
// Instantiate these inside the testbench (below); shown separately for clarity.
module fifo_scoreboard #(parameter WIDTH = 8, DEPTH = 8) (
input wire clk, rst,
input wire wr_en, full, rd_en, empty,
input wire [WIDTH-1:0] wdata, rdata
);
// Golden queue: a flat array with head/tail pointers = a software FIFO.
reg [WIDTH-1:0] q [0:1023]; // model_q storage
integer head, tail; // head=next pop, tail=next push
integer errors, pushes, pops;
reg [WIDTH-1:0] expected;
reg rd_fired; // read accepted last cycle
initial begin head = 0; tail = 0; errors = 0; pushes = 0; pops = 0; rd_fired = 0; end
always @(posedge clk) begin
if (rst) begin
head <= 0; tail <= 0; rd_fired <= 1'b0; // flush model on reset
end else begin
// 1) CHECK the read accepted last cycle (registered rdata valid now).
if (rd_fired) begin
expected = q[head]; // front of golden queue
head = head + 1; // q_pop
pops = pops + 1;
if (rdata !== expected) begin
$display("FAIL SCOREBOARD: rdata=%h expected=%h (order/dup/loss)", rdata, expected);
errors = errors + 1;
end
end
// 2) MIRROR an ACCEPTED write (wr_en AND not full) onto the queue back.
if (wr_en && !full) begin
q[tail] = wdata; // q_push
tail = tail + 1;
pushes = pushes + 1;
end
// 3) Latch whether a read is accepted THIS cycle for next-cycle check.
rd_fired <= (rd_en && !empty);
end
end
endmoduleIn VHDL the golden queue is an array plus head/tail pointers inside the process (or a shared variable protected type in a package); numeric_std handles the index arithmetic. The reference model pushes on an accepted write, pops on the previously-served read, and uses assert ... severity error as its self-check — the VHDL idiom that plays the role SystemVerilog's $error and Verilog's if (...) $display("FAIL") play.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity fifo_scoreboard is
generic ( WIDTH : positive := 8; DEPTH : positive := 8 );
port (
clk, rst : in std_logic;
wr_en, full : in std_logic; -- write side
wdata : in std_logic_vector(WIDTH-1 downto 0);
rd_en, empty : in std_logic; -- read side
rdata : in std_logic_vector(WIDTH-1 downto 0)
);
end entity;
architecture check of fifo_scoreboard is
type q_t is array (0 to 1023) of std_logic_vector(WIDTH-1 downto 0);
begin
process (clk)
variable model_q : q_t; -- golden queue storage
variable head : integer := 0; -- next pop
variable tail : integer := 0; -- next push
variable expected : std_logic_vector(WIDTH-1 downto 0);
variable rd_fired : std_logic := '0'; -- read accepted last cyc
begin
if rising_edge(clk) then
if rst = '1' then
head := 0; tail := 0; rd_fired := '0'; -- flush model on reset
else
-- 1) CHECK the read accepted last cycle (registered rdata valid now).
if rd_fired = '1' then
expected := model_q(head); -- front of golden queue
head := head + 1; -- q_pop
assert rdata = expected
report "SCOREBOARD mismatch: rdata /= expected (order/dup/loss)"
severity error;
end if;
-- 2) MIRROR an ACCEPTED write (wr_en AND not full) onto the back.
if (wr_en = '1') and (full = '0') then
model_q(tail) := wdata; -- q_push
tail := tail + 1;
end if;
-- 3) Latch whether a read is accepted THIS cycle.
if (rd_en = '1') and (empty = '0') then rd_fired := '1';
else rd_fired := '0'; end if;
end if;
end if;
end process;
end architecture;4b. The invariant assertions — the always-true guardrails
The scoreboard checks data; the invariants check structure — properties that must hold every cycle independent of the values. In SystemVerilog these are concurrent SVA properties bound alongside the DUT: occupancy bounded, flags mutually exclusive, flags agreeing with a running occupancy model, and every accepted operation legal. occ here is a tiny running occupancy the checker maintains from the DUT's own accepted operations.
module fifo_invariants #(parameter int DEPTH = 8) (
input logic clk, rst,
input logic wr_en, full, rd_en, empty
);
// A running occupancy the checker derives from ACCEPTED ops (its own oracle).
int occ = 0;
wire do_write = wr_en & ~full;
wire do_read = rd_en & ~empty;
always_ff @(posedge clk)
if (rst) occ <= 0;
else if ( do_write & ~do_read) occ <= occ + 1; // write only -> +1
else if (~do_write & do_read) occ <= occ - 1; // read only -> -1
// both / idle -> unchanged (simultaneous read+write is net zero)
// INVARIANT 1: occupancy never leaves 0..DEPTH (no overrun, no underrun).
a_bounds: assert property (@(posedge clk) disable iff (rst)
(occ >= 0) && (occ <= DEPTH))
else $error("occupancy %0d out of 0..%0d", occ, DEPTH);
// INVARIANT 2: full and empty are never both asserted.
a_excl: assert property (@(posedge clk) disable iff (rst)
!(full && empty))
else $error("full AND empty asserted together");
// INVARIANT 3: the flags AGREE with the derived occupancy (7.2 boundary check).
a_empty: assert property (@(posedge clk) disable iff (rst)
empty == (occ == 0))
else $error("empty=%b but occ=%0d", empty, occ);
a_full: assert property (@(posedge clk) disable iff (rst)
full == (occ == DEPTH))
else $error("full=%b but occ=%0d", full, occ);
// INVARIANT 4: an accepted write requires !full; an accepted read requires !empty.
a_wr_legal: assert property (@(posedge clk) disable iff (rst)
(wr_en && full) |-> $stable(occ) || do_read)
else $error("write accepted while full");
endmoduleEach assert property is a guardrail that fires on the exact cycle it is violated. Invariant 3 is the one that would have caught a 7.2 boundary bug on its own: if full asserts one slot early or one slot late, full == (occ == DEPTH) breaks and names the cycle. Verilog has no concurrent assertions, so the same invariants become procedural if-checks inside a clocked always block — a check_invariants step run every cycle that increments an error counter and prints on violation.
// Procedural invariant checker: fold this into the testbench's clocked block, or
// instantiate it. Derives its own occupancy from accepted ops and checks 4 rules.
module fifo_invariants #(parameter DEPTH = 8) (
input wire clk, rst, wr_en, full, rd_en, empty
);
integer occ, errors;
wire do_write = wr_en & ~full;
wire do_read = rd_en & ~empty;
initial begin occ = 0; errors = 0; end
always @(posedge clk) begin
if (rst) occ <= 0;
else begin
// update the derived occupancy (simultaneous rd+wr is net zero)
if ( do_write & ~do_read) occ <= occ + 1;
else if (~do_write & do_read) occ <= occ - 1;
// INVARIANT 1: bounds. INVARIANT 2: mutual exclusion.
if (occ < 0 || occ > DEPTH) begin
$display("FAIL: occupancy %0d out of 0..%0d", occ, DEPTH); errors = errors + 1;
end
if (full && empty) begin
$display("FAIL: full AND empty together"); errors = errors + 1;
end
// INVARIANT 3: flags must AGREE with occupancy (7.2 boundary check).
if (empty !== (occ == 0)) begin
$display("FAIL: empty=%b but occ=%0d", empty, occ); errors = errors + 1;
end
if (full !== (occ == DEPTH)) begin
$display("FAIL: full=%b but occ=%0d", full, occ); errors = errors + 1;
end
// INVARIANT 4: no write accepted when full (would-be overrun).
if (wr_en && full && !do_read && !do_write) ; // refused correctly: ok
end
end
endmoduleIn VHDL the invariants are assert ... report ... severity error statements inside the clocked process — VHDL's native check. The derived occupancy is an integer, and each rule is one assert, firing on the cycle it breaks.
library ieee;
use ieee.std_logic_1164.all;
entity fifo_invariants is
generic ( DEPTH : positive := 8 );
port ( clk, rst, wr_en, full, rd_en, empty : in std_logic );
end entity;
architecture check of fifo_invariants is
signal do_write, do_read : std_logic;
begin
do_write <= wr_en and not full;
do_read <= rd_en and not empty;
process (clk)
variable occ : integer := 0;
begin
if rising_edge(clk) then
if rst = '1' then
occ := 0;
else
if (do_write = '1') and (do_read = '0') then occ := occ + 1;
elsif (do_write = '0') and (do_read = '1') then occ := occ - 1;
end if; -- both/idle: unchanged
-- INVARIANT 1: occupancy in 0..DEPTH (no overrun/underrun).
assert (occ >= 0) and (occ <= DEPTH)
report "occupancy out of 0..DEPTH" severity error;
-- INVARIANT 2: never full and empty at once.
assert not (full = '1' and empty = '1')
report "full AND empty asserted together" severity error;
-- INVARIANT 3: flags AGREE with occupancy (7.2 boundary).
assert (empty = '1') = (occ = 0)
report "empty flag disagrees with occupancy" severity error;
assert (full = '1') = (occ = DEPTH)
report "full flag disagrees with occupancy" severity error;
end if;
end if;
end process;
end architecture;4c. Directed corners + constrained-random driver — the self-checking top
Now the top-level testbench that drives the corners, then unleashes constrained-random traffic, all judged by the 4a scoreboard and 4b invariants, ending in a PASS/FAIL summary. The SystemVerilog version binds the scoreboard and invariant checkers to the DUT, runs the directed corners (fill-to-full, drain-to-empty, simultaneous read+write, reset mid-operation, wrap boundary), then randomizes wr_en/rd_en with independent backpressure for thousands of cycles.
module fifo_verify_tb;
localparam int WIDTH = 8, DEPTH = 8;
logic clk = 0, rst = 1, wr_en = 0, rd_en = 0;
logic [WIDTH-1:0] wdata = 0, rdata;
logic full, empty;
sync_fifo #(.WIDTH(WIDTH), .DEPTH(DEPTH)) dut (
.clk(clk), .rst(rst), .wr_en(wr_en), .wdata(wdata), .full(full),
.rd_en(rd_en), .rdata(rdata), .empty(empty));
// Bind the golden-queue scoreboard and the invariant checker to the DUT.
fifo_scoreboard #(.WIDTH(WIDTH), .DEPTH(DEPTH)) sb (
.clk(clk), .rst(rst), .wr_en(wr_en), .full(full), .wdata(wdata),
.rd_en(rd_en), .empty(empty), .rdata(rdata));
fifo_invariants #(.DEPTH(DEPTH)) inv (
.clk(clk), .rst(rst), .wr_en(wr_en), .full(full), .rd_en(rd_en), .empty(empty));
always #5 clk = ~clk; // 100 MHz
initial begin
@(negedge clk); rst = 0;
// CORNER: fill to full, confirm the surplus write is refused (no overrun).
for (int i = 0; i < DEPTH; i++) begin
@(negedge clk); wr_en = 1; wdata = i[WIDTH-1:0];
end
@(negedge clk); wr_en = 1; wdata = 8'hFF; // write-when-FULL: must refuse
@(negedge clk); wr_en = 0;
// CORNER: simultaneous read+write while partially full (occupancy holds).
repeat (4) begin @(negedge clk); wr_en = 1; rd_en = 1; wdata = $urandom; end
@(negedge clk); wr_en = 0; rd_en = 0;
// CORNER: drain to empty, confirm the surplus read is refused (no underrun).
for (int i = 0; i < DEPTH + 2; i++) begin @(negedge clk); rd_en = 1; end
@(negedge clk); rd_en = 0;
// CORNER: reset mid-operation. Push a few, assert rst, both must flush.
repeat (3) begin @(negedge clk); wr_en = 1; wdata = $urandom; end
@(negedge clk); wr_en = 0; rst = 1; // reset while data in flight
@(negedge clk); rst = 0;
// CONSTRAINED-RANDOM: independent backpressure for many cycles. This is what
// schedules the simultaneous read+write at the wrap boundary the corners miss.
for (int t = 0; t < 5000; t++) begin
@(negedge clk);
wr_en = ($urandom_range(0,99) < 60); // 60% write pressure
rd_en = ($urandom_range(0,99) < 55); // 55% read pressure (INDEPENDENT)
wdata = $urandom;
end
@(negedge clk); wr_en = 0; rd_en = 0;
repeat (DEPTH+2) @(negedge clk); // let final reads drain+check
// SELF-CHECKING SUMMARY from the scoreboard.
if (sb.errors == 0)
$display("PASS: scoreboard clean over %0d pushes / %0d pops (order/no-loss/no-dup)",
sb.pushes, sb.pops);
else
$display("FAIL: %0d scoreboard mismatches", sb.errors);
$finish;
end
endmoduleThe directed corners prove the FIFO can do each dangerous thing; the 5000-cycle constrained-random block with independent write and read pressure is what actually hits the simultaneous-read-and-write-at-the-wrap-boundary collision — and because the scoreboard is bound the whole time, that collision is checked the instant it happens. The Verilog top is the same shape without SVA: it instantiates the array-queue scoreboard and the procedural invariant checker, runs the corners, then a $random-driven independent-backpressure loop, and prints PASS/FAIL from the scoreboard's error count.
module fifo_verify_tb;
parameter WIDTH = 8, DEPTH = 8, AW = 3;
reg clk, rst, wr_en, rd_en;
reg [WIDTH-1:0] wdata;
wire [WIDTH-1:0] rdata;
wire full, empty;
integer i, t;
sync_fifo #(.WIDTH(WIDTH), .DEPTH(DEPTH), .AW(AW)) dut (
.clk(clk), .rst(rst), .wr_en(wr_en), .wdata(wdata), .full(full),
.rd_en(rd_en), .rdata(rdata), .empty(empty));
// Golden-queue scoreboard + procedural invariants bound to the DUT.
fifo_scoreboard #(.WIDTH(WIDTH), .DEPTH(DEPTH)) sb (
.clk(clk), .rst(rst), .wr_en(wr_en), .full(full),
.rd_en(rd_en), .empty(empty), .wdata(wdata), .rdata(rdata));
fifo_invariants #(.DEPTH(DEPTH)) inv (
.clk(clk), .rst(rst), .wr_en(wr_en), .full(full), .rd_en(rd_en), .empty(empty));
always #5 clk = ~clk;
initial begin
clk = 0; rst = 1; wr_en = 0; rd_en = 0; wdata = 0;
@(negedge clk); rst = 0;
// CORNER: fill to full, then a write-when-FULL that must be refused.
for (i = 0; i < DEPTH; i = i + 1) begin
@(negedge clk); wr_en = 1; wdata = i;
end
@(negedge clk); wr_en = 1; wdata = 8'hFF; // must be refused (no overrun)
@(negedge clk); wr_en = 0;
// CORNER: simultaneous read+write while partially full.
for (i = 0; i < 4; i = i + 1) begin
@(negedge clk); wr_en = 1; rd_en = 1; wdata = $random;
end
@(negedge clk); wr_en = 0; rd_en = 0;
// CORNER: drain to empty, then a read-when-EMPTY that must be refused.
for (i = 0; i < DEPTH + 2; i = i + 1) begin @(negedge clk); rd_en = 1; end
@(negedge clk); rd_en = 0;
// CORNER: reset mid-operation (model and DUT both flush).
for (i = 0; i < 3; i = i + 1) begin @(negedge clk); wr_en = 1; wdata = $random; end
@(negedge clk); wr_en = 0; rst = 1;
@(negedge clk); rst = 0;
// CONSTRAINED-RANDOM: INDEPENDENT backpressure for many cycles.
for (t = 0; t < 5000; t = t + 1) begin
@(negedge clk);
wr_en = (($random % 100) + 100) % 100 < 60; // ~60% write pressure
rd_en = (($random % 100) + 100) % 100 < 55; // ~55% read pressure (independent)
wdata = $random;
end
@(negedge clk); wr_en = 0; rd_en = 0;
for (i = 0; i < DEPTH + 2; i = i + 1) @(negedge clk); // drain + check tail
// SELF-CHECKING SUMMARY.
if (sb.errors == 0)
$display("PASS: scoreboard clean over %0d pushes / %0d pops (order/no-loss/no-dup)",
sb.pushes, sb.pops);
else
$display("FAIL: %0d scoreboard mismatches", sb.errors);
$finish;
end
endmoduleThe VHDL top instantiates the same scoreboard and invariant checkers, drives the corners, then runs a constrained-random loop using a simple LCG for pseudo-random wr_en/rd_en (independent seeds), and ends with a report ... severity note summary — the scoreboard's own asserts having already flagged any mismatch at its exact cycle.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity fifo_verify_tb is
end entity;
architecture sim of fifo_verify_tb is
constant WIDTH : positive := 8;
constant DEPTH : positive := 8;
constant AW : positive := 3;
signal clk : std_logic := '0';
signal rst : std_logic := '1';
signal wr_en : std_logic := '0';
signal rd_en : std_logic := '0';
signal wdata : std_logic_vector(WIDTH-1 downto 0) := (others => '0');
signal rdata : std_logic_vector(WIDTH-1 downto 0);
signal full : std_logic;
signal empty : std_logic;
begin
dut : entity work.sync_fifo
generic map (WIDTH => WIDTH, DEPTH => DEPTH, AW => AW)
port map (clk => clk, rst => rst, wr_en => wr_en, wdata => wdata,
full => full, rd_en => rd_en, rdata => rdata, empty => empty);
-- Golden-queue scoreboard + invariant checker bound to the DUT.
sb : entity work.fifo_scoreboard
generic map (WIDTH => WIDTH, DEPTH => DEPTH)
port map (clk => clk, rst => rst, wr_en => wr_en, full => full, wdata => wdata,
rd_en => rd_en, empty => empty, rdata => rdata);
inv : entity work.fifo_invariants
generic map (DEPTH => DEPTH)
port map (clk => clk, rst => rst, wr_en => wr_en, full => full,
rd_en => rd_en, empty => empty);
clk <= not clk after 5 ns;
stim : process
variable seed_w : unsigned(31 downto 0) := x"12345678"; -- LCG state (write)
variable seed_r : unsigned(31 downto 0) := x"9E3779B9"; -- LCG state (read, independent)
variable i : integer;
begin
wait until falling_edge(clk); rst <= '0';
-- CORNER: fill to full, then a write-when-FULL that must be refused.
for i in 0 to DEPTH-1 loop
wait until falling_edge(clk);
wr_en <= '1'; wdata <= std_logic_vector(to_unsigned(i, WIDTH));
end loop;
wait until falling_edge(clk); wr_en <= '1'; wdata <= x"FF"; -- refused
wait until falling_edge(clk); wr_en <= '0';
-- CORNER: simultaneous read+write while partially full.
for i in 0 to 3 loop
wait until falling_edge(clk); wr_en <= '1'; rd_en <= '1';
end loop;
wait until falling_edge(clk); wr_en <= '0'; rd_en <= '0';
-- CORNER: drain to empty, then a read-when-EMPTY that must be refused.
for i in 0 to DEPTH+1 loop
wait until falling_edge(clk); rd_en <= '1';
end loop;
wait until falling_edge(clk); rd_en <= '0';
-- CORNER: reset mid-operation.
for i in 0 to 2 loop
wait until falling_edge(clk); wr_en <= '1';
end loop;
wait until falling_edge(clk); wr_en <= '0'; rst <= '1';
wait until falling_edge(clk); rst <= '0';
-- CONSTRAINED-RANDOM: independent LCG backpressure for many cycles.
for i in 0 to 4999 loop
wait until falling_edge(clk);
seed_w := seed_w * 1103515245 + 12345; -- advance write LCG
seed_r := seed_r * 1103515245 + 12345; -- advance read LCG (independent)
if to_integer(seed_w(30 downto 24)) < 76 then wr_en <= '1'; else wr_en <= '0'; end if;
if to_integer(seed_r(30 downto 24)) < 70 then rd_en <= '1'; else rd_en <= '0'; end if;
wdata <= std_logic_vector(seed_w(WIDTH-1 downto 0));
end loop;
wait until falling_edge(clk); wr_en <= '0'; rd_en <= '0';
for i in 0 to DEPTH+1 loop wait until falling_edge(clk); end loop; -- drain + check
report "fifo_verify self-check complete (scoreboard asserts any mismatch inline)" severity note;
wait;
end process;
end architecture;Across all three languages the lesson is one sentence: a FIFO is proven correct only when a reference-model scoreboard — a golden queue checking order, no-loss, and no-duplication — agrees with the DUT across the directed corners AND thousands of cycles of constrained-random traffic with independent backpressure, while the invariant assertions hold on every cycle.
5. Verification Strategy
This section is the methodology itself — the plan the §4 environment implements. A FIFO's correctness is a stream property: whatever is written must be read back in the same order, with no loss and no duplication, and the flags must always tell the truth about occupancy. That property is not provable by inspection; it is provable only by the combination below, and the difference between directed "it works" and scoreboard-checked "it's proven" is that the directed test confirms one trajectory while the scoreboard confirms every accepted operation on every cycle it runs.
- The scoreboard is the proof engine. Keep a reference-model queue and drive it from accepted operations:
pushonwr_en && !full,poponrd_en && !empty, and on every pop assertrdata == expected(one cycle late for the registered read). This single check simultaneously proves ordering (a reorder pops the wrong value), no-loss (a dropped word leaves the model longer than the DUT delivers), and no-duplication (a repeated word makes the DUT return a value the model already popped). Directed "write N, read N" proves none of these under interleaving; the scoreboard proves all three continuously. - The invariants that must hold every cycle. Encode them as assertions (SVA in SV,
if-checks in Verilog,assert ... severityin VHDL): (i) occupancy always in[0, DEPTH]— never negative (underrun), never aboveDEPTH(overrun); (ii) neverfullandemptyat once; (iii)emptyis true exactly when occupancy is 0 andfullexactly when occupancy isDEPTH— the check that catches a 7.2 boundary bug directly; (iv) a write is accepted only when!fulland a read served only when!empty. Invariants are cheap, always-on, and name the exact failing cycle. - The directed corner list — driven on purpose. The scoreboard only judges cycles you drive, so drive them all: fill-to-full (next write refused, no overrun); drain-to-empty (next read refused, no underrun); simultaneous read+write on a partially-full FIFO (occupancy unchanged — the both-at-once case); write-when-full rejected and read-when-empty rejected (the 7.1 gates); reset mid-operation (pointers, count, and model all flush; FIFO reads empty); and the pointer-wrap boundary (roll a pointer past
DEPTH-1so the equal-pointer full/empty distinction of 7.2 is exercised). Each corner is one deliberate stimulus; each is where a real FIFO breaks. - Constrained-random covers the corners you didn't enumerate. Randomize
wr_enandrd_enwith independent backpressure and run thousands of cycles against the same scoreboard and invariants. Independence is essential: correlated stimulus (strict alternation) never collides a read and a write on the same cycle, so it silently reproduces the directed test. Independent pressure eventually schedules the simultaneous read+write at the wrap boundary — the exact timing §7's bug needs — and the scoreboard is already watching. Add coverage that confirms the random run actually hit full, empty, simultaneous-rw, and the wrap. - Parameter-generic verification. A FIFO is configurable, so verify it generic: re-run the whole environment for several
WIDTH(1, 8, 32) andDEPTH(2, 4, 16) including a small depth (where the boundary is easiest to break) and a wrap-around. A FIFO that passes atDEPTH=8can still be wrong atDEPTH=2if the flag comparison orcountwidth was sloppy. - The line between "it works" and "it's proven." "It works" is a single directed trajectory checked at one endpoint — the RTL author's fill-then-drain. "It's proven" is a passive oracle (the scoreboard) plus always-true guardrails (the invariants) plus deliberate corners plus long random traffic, all passing. The two look similar on a good day and diverge exactly on the one-in-ten-thousand cycle that ships broken. A pattern ships with its proof; the proof is this environment, not a clean waveform.
6. Common Mistakes
Spot-checking instead of scoreboarding. The signature verification failure and the whole reason FIFOs ship broken. Writing a few words, reading a few back, and eyeballing that they match confirms one trajectory and nothing about interleaving — it misses every corner bug because it never drives the corner. A spot check has no oracle: there is no golden queue to disagree with, so ordering, duplication, and loss under load go unchecked. The fix is architectural, not effortful: keep a reference-model queue, drive it from accepted operations, and assert rdata == expected on every served read. The scoreboard costs about the same to write as the spot check and proves a categorically stronger property.
No simultaneous read+write test. A FIFO's most delicate cycle is the one where a push and a pop land on the same clock edge — occupancy must stay unchanged, and the count update and the pointer logic must both handle it. A testbench that only ever writes-then-reads (or strictly alternates) never drives this cycle, so a both-at-once bug survives verification untouched. Drive it directly in the corners and let constrained-random hit it with independent backpressure; a scoreboard that never sees a simultaneous operation has not verified the FIFO.
Not testing reset mid-operation. Resetting an empty FIFO proves almost nothing — the hard case is asserting reset while data is in flight and pointers are non-zero. A FIFO that clears its memory but leaves pointers stale (the Project-C bug from the overview) reads garbage for a few cycles after reset, and only a mid-operation reset test catches it. The testbench must push a few words, assert reset, flush the scoreboard to match, and confirm the FIFO reads empty with the model back in step.
Not checking the exact full/empty boundary (7.2). The equal-pointer boundary is where full is distinguished from empty, and an off-by-one there — full asserting one slot early or late — passes a casual test but drops or admits one word at the edge. The invariant full == (occ == DEPTH) (and empty == (occ == 0)) checks this every cycle; a testbench that never fills to exactly DEPTH or drains to exactly 0 while watching the flags leaves the boundary unverified. Fill and drain to the exact edge and assert the flag flips on the right cycle.
Checking data but not ORDER (or not no-duplication). A weak scoreboard that only checks "every word I read was some word I wrote" (a set/multiset compare) misses reordering and can miss duplication. FIFO correctness is ordered: the reference must be a queue, popped front-to-back, so the sequence is checked, not just membership. A duplicate — the same word returned twice — must make the model run empty early or mismatch; a set-based check would wave it through. Use an in-order queue and compare position by position.
No random stimulus, so the boundary collisions never occur. Directed tests only exercise the interleavings you thought of. The simultaneous-read-and-write-at-the-wrap-boundary collision that duplicates a word (the §7 bug) is not on anyone's directed list because you don't design a bug on purpose — you stumble onto it under randomized traffic. Without a long constrained-random run with independent backpressure, that cycle is never scheduled and the bug ships. Random stimulus is not optional polish; it is the only thing that finds the collision the directed corners cannot enumerate.
7. DebugLab
The FIFO that passed every directed test and still duplicated a word
The engineering lesson: "it simulated" is not "it's verified" — a FIFO is only proven correct by a reference-model scoreboard that checks order, no-loss, and no-duplication across the corners and constrained-random stimulus. The tell is a bug that is green in the lab and red in silicon, surfacing as a rare, load-dependent duplication or loss no directed test reproduces: that fingerprint means the verification never scheduled the collision, not that the FIFO is unlucky. A directed "write N, read N" test answers does it work?; only a golden-queue scoreboard under independent-backpressure random traffic answers is it proven? — and that is the difference between the four hand-written FIFOs that each shipped a different bug and the one proven FIFO you reuse with confidence.
8. Interview Q&A
9. Exercises
Design and reasoning exercises — no syntax drills. Each rehearses the "prove it, don't spot-check it" habit.
Exercise 1 — Classify the checks
For each proposed check, state whether it belongs to the scoreboard, an invariant assertion, a directed corner, or the constrained-random driver, and why in one line: (a) assert rdata == model_q.pop_front() on every served read; (b) assert !(full && empty) every cycle; (c) push exactly DEPTH words then confirm the next push is refused; (d) randomize wr_en/rd_en at 60%/55% independent for 5000 cycles; (e) assert full == (occ == DEPTH) every cycle; (f) assert reset while three words are in flight and confirm the FIFO reads empty. (Hint: passive-oracle vs always-true-guardrail vs deliberate-stimulus.)
Exercise 2 — Why the spot check passes
The RTL author's test writes 0..7, reads eight back, and prints PASS, yet the FIFO duplicates a word one time in ten thousand in the field. Explain precisely (i) which specific cycle-timing the failing case requires, (ii) exactly why the fill-then-drain test can never produce that timing, and (iii) why even if it did, the test would still not catch the bug (what is missing besides the stimulus). Then name the two additions that together turn the spot check into a proof.
Exercise 3 — Model the accepted operations
You are writing a scoreboard and, to save a line, you decide to push onto the golden queue on the bare wr_en and pop on the bare rd_en, ignoring full/empty. Describe the first cycle on which your model diverges from the DUT for (i) a write requested while full and (ii) a read requested while empty, and what false failure the scoreboard then reports. State the one-line correction and why it keeps the model in lockstep with the DUT's real contents.
Exercise 4 — Independent vs correlated backpressure
Two verification engineers both add "random" stimulus. Engineer A drives rd_en = ~wr_en (strict alternation). Engineer B drives wr_en and rd_en from two independent random sources. (i) Explain why Engineer A's stimulus, despite looking random, can never expose the simultaneous-read+write-at-the-boundary bug. (ii) Explain what Engineer B's independence buys that A's lacks. (iii) Name one coverage point you would add to confirm that B's run actually hit the simultaneous-rw-at-wrap case, so a green result is trustworthy rather than lucky.
10. Related Tutorials
Continue in RTL Design Patterns (forward links unlock as they ship):
- FIFO Full/Empty Logic — Chapter 7.2 (flagship); the exact pointer-based full/empty boundary this page's invariant
full == (occ == DEPTH)is written to catch. - FIFO Programmable Flags — Chapter 7.3; almost-full / almost-empty thresholds — extra flags the scoreboard and invariants extend to cover.
- FIFO Depth Calculation — Chapter 7.4; how to size
DEPTHfor a burst — the parameter this environment must be re-run generic across. - First-Word-Fall-Through FIFO — Chapter 7.5; the zero-read-latency variant, where the scoreboard compares
rdatathe same cycle instead of one late. - valid/ready Handshake — Chapter 9.1 (flagship); the generic back-pressure protocol whose independent stimulus this page's constrained-random driver rehearses.
- Asynchronous FIFO — Chapter 11.6 (flagship); the same FIFO across two clocks, verified with a scoreboard plus clock-domain-crossing checks.
Backward / composes these patterns:
- Synchronous FIFO Architecture — Chapter 7.1; the DUT this page verifies — the circular buffer whose ordering and no-loss the scoreboard proves.
- The RTL Design Mindset — Chapter 0.2; the Verification lens of Interface → State → Datapath → Control → Verification, made concrete here.
- What Is an RTL Design Pattern? — Chapter 0.1; the four-FIFO opening DebugLab — four teams, four bugs — that this page's methodology is the answer to.
- The Register Pattern (D-FF) — Chapter 2.1; the clocked, reset update the scoreboard and invariant checkers are themselves built from.
- Comparators — Chapter 1.x; the equality compares (
occ == DEPTH,occ == 0) the invariant assertions rest on. - Synchronous Reset — Chapter 2.x; the reset the "reset mid-operation" corner exercises, and that the scoreboard must flush to match.
Verilog v1 prerequisites (the grammar this environment transcribes into):
- Blocking and Non-Blocking Assignments — why the scoreboard's clocked checks use non-blocking updates and sample
rdataone cycle after a served read. - Case Statements — the both-at-once occupancy update the simultaneous-read+write corner exercises.
- Physical Data Types — the array (
reg [WIDTH-1:0] q [0:1023]) that becomes the Verilog golden queue. - Race Conditions & Determinism — why the testbench drives on
negedgeand samples onposedgeso the scoreboard reads settled values. - initial and always Blocks — the
initialstimulus process and the clockedalwaysscoreboard the environment is built from.
11. Summary
- "It simulated" is not "it's verified." A directed "write N, read N" spot check confirms one trajectory at one endpoint; a FIFO is proven correct only by a reference-model scoreboard, invariant assertions, directed corners, and constrained-random stimulus, all passing. The two look alike on a good day and diverge on the one-in-ten-thousand cycle that ships broken.
- The scoreboard is a golden shadow queue. Push on every accepted write (
wr_en && !full), pop on every served read (rd_en && !empty), and assertrdata == expected(one cycle late for the registered read). One check proves ordering, no-loss, and no-duplication at once — because the reference is an ordered queue popped front-to-back, not a set. Model accepted operations, never bare requests, or the model drifts and every check is a false alarm. - Invariants are the always-true guardrails. Occupancy always in
[0, DEPTH]; neverfullandemptyat once;empty == (occ == 0)andfull == (occ == DEPTH)(the check that catches a 7.2 boundary off-by-one); accepted ops are legal. Encode them as SVA in SystemVerilog, proceduralif-checks in Verilog,assert ... severityin VHDL — firing on the exact violating cycle. - Directed corners are driven on purpose; random finds the rest. Drive fill-to-full, drain-to-empty, simultaneous read+write, write-when-full and read-when-empty rejection, reset mid-operation, and the pointer-wrap boundary. Then run constrained-random
wr_en/rd_enwith independent backpressure for thousands of cycles — the only thing that schedules the simultaneous-read+write-at-the-boundary collision the directed corners cannot enumerate. - The bug only the scoreboard catches. A FIFO can pass every directed test and still duplicate or drop a word on the simultaneous-read-and-write-at-the-wrap-boundary case — green in the lab, one packet in ten thousand in the field. The golden-queue scoreboard under independent-backpressure random stimulus flags the exact cycle
rdatadiverges from expected, turning a three-month field mystery into a seconds-long simulation failure. A pattern ships with its proof — self-checking environments shown here in SystemVerilog, Verilog, and VHDL.