Four mechanisms break independently. Overflow drops data, underflow returns garbage, count drift corrupts flags at wrap, and wrong bytes pass every occupancy check.
Watch count rise with push, then fall with pop; full and empty follow the count.
Slot 0: empty; the first push arrives.
Slot 1: count 1; still empty-free and far from full.
Slot 2: count 2; pushes continue.
Slot 3: count 3; one slot remains.
Slot 4: count 4, so full rises; pushes stop and pops begin.
Slot 5: count 3; full clears on the first drain.
Slot 6: count 2; draining continues.
Slot 7: count 1; one more pop reaches empty.
Failure | Rule that catches it |
|---|---|
Overflow |
|
Underflow |
|
Bookkeeping drift | Count follows accepted push minus accepted pop |
Data corruption | Popped bytes match pushed bytes in order |
The data-integrity rule needs the push from as many pushes back as the FIFO holds. The textbook form is one gated $past(din, k, push) per occupancy; Verilator 5.048 rejects the gate, so this checker keeps the expected order in a queue written as modeling code, which works for any occupancy. The count rule writes ~full and ~empty, because Verilator also rejects ! anywhere after ##1.
The listing is one file you can paste into the Code Lab: the checker first, then a small design and a bench that runs legal traffic before planting one bug at a time. Every rule reports through fail(), which counts and prints the report and lets the run go on; Verilator 5.048 stops at the first $error, and production checkers often count the same way.
module fifo_checker #(
parameter int DEPTH = 16,
parameter int DW = 32,
parameter int PTR_W = $clog2(DEPTH),
parameter int MAX_DRAIN = 1024
)(
input logic clk, rst_n,
input logic push, pop, full, empty,
input logic [PTR_W:0] count,
input logic [PTR_W:0] wr_ptr, rd_ptr,
input logic [DW-1:0] din, dout
);
int n_fail = 0, n_wrap = 0, n_drain = 0;
function automatic void fail(string msg);
n_fail++;
$display("[%0t] fifo_checker: %s", $time, msg);
endfunction
// Simultaneous push and pop at full is legal here (net zero).
a_no_overflow: assert property (@(posedge clk) disable iff (!rst_n)
(push && !pop) |-> !full)
else fail("push while full");
a_no_underflow: assert property (@(posedge clk) disable iff (!rst_n)
pop |-> !empty)
else fail("pop while empty");
// Accepted push needs room or a simultaneous pop; accepted pop needs data.
// "~" rather than "!": Verilator 5.048 rejects "!" anywhere after ##1.
a_count_delta: assert property (@(posedge clk) disable iff (!rst_n)
##1 count == $past(count)
+ (PTR_W+1)'($past(push && (pop || ~full)))
- (PTR_W+1)'($past(pop && ~empty)))
else fail("count drifted from push/pop history");
// Free-running pointers with an extra MSB; truncated indexes alias full and empty.
a_ptr_count: assert property (@(posedge clk) disable iff (!rst_n)
count == (PTR_W+1)'(wr_ptr - rd_ptr))
else fail("count disagrees with the pointers");
a_empty_def: assert property (@(posedge clk) disable iff (!rst_n)
empty == (count == 0)) else fail("empty flag wrong");
a_full_def: assert property (@(posedge clk) disable iff (!rst_n)
full == (count == DEPTH)) else fail("full flag wrong");
a_excl: assert property (@(posedge clk) disable iff (!rst_n)
!(empty && full)) else fail("full and empty together");
// Data integrity. The distance back is the occupancy, so instead of
// $past(din, k, push) for every k, a queue in modeling code keeps the order.
logic [DW-1:0] expect_q [$];
always @(posedge clk)
if (!rst_n) expect_q.delete();
else begin
if (pop && !empty && expect_q.size() != 0) void'(expect_q.pop_front());
if (push && (pop || !full)) expect_q.push_back(din);
end
a_data: assert property (@(posedge clk) disable iff (!rst_n)
(pop && !empty) |-> dout == expect_q[0])
else fail("popped data out of order or corrupted");
c_wrap: cover property (@(posedge clk)
$past(wr_ptr[PTR_W-1:0]) == DEPTH-1 && wr_ptr[PTR_W-1:0] == 0) n_wrap++;
c_full_to_empty: cover property (@(posedge clk)
full ##[1:MAX_DRAIN] empty) n_drain++;
endmodule
// A small synchronous FIFO with free-running pointers and two plantable bugs.
module sfifo #(
parameter int DW = 8,
parameter int DEPTH = 8,
parameter int AW = $clog2(DEPTH)
)(
input logic clk, rst_n, push, pop,
input logic [1:0] bug, // 0 none, 1 corrupt one read, 2 count a blocked push
input logic [DW-1:0] din,
output logic [DW-1:0] dout,
output logic full, empty,
output logic [AW:0] count, wptr, rptr
);
logic [DW-1:0] mem [DEPTH];
wire push_ok = push && (!full || pop);
wire pop_ok = pop && !empty;
assign full = (count == DEPTH);
assign empty = (count == 0);
assign dout = mem[rptr[AW-1:0]] ^ (bug == 1 ? 8'h80 : 8'h00);
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) begin wptr <= 0; rptr <= 0; count <= 0; end
else begin
if (push_ok) begin mem[wptr[AW-1:0]] <= din; wptr <= wptr + 1; end
if (pop_ok) rptr <= rptr + 1;
count <= count + (push_ok || (bug == 2 && push) ? 1 : 0) - (pop_ok ? 1 : 0);
end
endmodule
legal traffic: fill, pass-through at full, drain, stream: 0 new report(s)
covers: pointer wrap 2, full-to-empty 1
[275] fifo_checker: pop while empty
pop while empty: 1 new report(s)
[295] fifo_checker: popped data out of order or corrupted
a corrupted read: 1 new report(s)
[385] fifo_checker: push while full
[395] fifo_checker: count disagrees with the pointers
[395] fifo_checker: count drifted from push/pop history
[405] fifo_checker: count disagrees with the pointers
push while full into a DUT that counts it: 4 new report(s)
PASS: legal traffic hit both covers, and every planted bug was reportedThe textbook general check uses local variables, one thread per word in flight. That full form lives in the advanced local-variables lesson; the per-occupancy loop above covers fixed occupancy.
Gray pointers for async FIFOs are a same-domain check. Assert the one-bit step in the pointer's own domain, never occupancy across clocks.
// snippet
// Same-domain Gray step with reset and first-cycle guards:
// a_gray_step: assert property (@(posedge clk) disable iff (!rst_n)
// !$isunknown(gray_ptr) && !$isunknown($past(gray_ptr)) |->
// ($countones($past(gray_ptr) ^ gray_ptr) <= 1));push and pop arrive together while full is high. Does the overflow rule fire?No. The antecedent push && !pop excludes the simultaneous case, whose net occupancy change is zero.
$clog2(DEPTH) bits. What breaks at wrap?Full aliases empty. Equal indexes read as both, so the flag rules corrupt; the extra MSB keeps one lap of history.
Fill, a push and pop together at full, drain, and a primed stream give no reports, and both covers hit: the pointers wrapped twice and the FIFO went from full to empty. A pop while empty and a corrupted read each give one report. A push while full into a design that wrongly counts it gives four: the protocol rule names the push, then the count and pointer rules disagree for two cycles. The first report is again the one to read.
Run with Verilator 5.048 (--binary --timing --assert, plus --coverage when a listing has a cover property) on 2026-10-18; every bench printed the PASS line shown. Verilator stops at the first $error or failing assertion without an action block, so the benches count failures in the action block. Icarus 13 has no concurrent assertions.
The textbook per-occupancy gated $past was replaced by a queue in modeling code; the count rule writes ~full and ~empty because Verilator 5.048 rejects ! after ##1.