The design below implements the conservative registered-output contract. The parameterized finite harness defaults to depth 5, runs directed boundaries and reset epochs, forces pointer wrap, and compares 3000 pseudo-random cycles against an independent reference queue.
Read the picture from the top: the same accepted operations reach both the DUT and the reference, so any difference shows up at the compare.
The reference is independent. It is a plain queue, not a copy of the RTL, so a shared bug cannot hide.
The compare checks order. Each result is matched against the next expected word, which catches loss, duplication and reordering.
Assertions see inside. They check rules the outputs alone cannot show, such as a pointer holding when its request is refused.
module sync_fifo #(
parameter int DW = 8,
parameter int DEPTH = 16,
parameter int AF_MARGIN = 2,
parameter int AE_MARGIN = 1
) (
input logic clk,
input logic rst_n,
input logic push_i,
input logic pop_i,
input logic [DW-1:0] din_i,
output logic [DW-1:0] dout_o,
output logic dout_valid_o,
output logic full_o,
output logic empty_o,
output logic almost_full_o,
output logic almost_empty_o,
output logic [$clog2(DEPTH+1)-1:0] level_o
);
localparam int AW = (DEPTH <= 1) ? 1 : $clog2(DEPTH);
localparam int CW = $clog2(DEPTH + 1);
logic [DW-1:0] mem [0:DEPTH-1];
logic [AW-1:0] wr_ptr, rd_ptr;
logic [CW-1:0] count;
logic push_take, pop_take;
// Elaboration-time guards: an illegal configuration fails to build.
if (DEPTH < 2) begin : g_bad_depth
$error("DEPTH must be at least 2");
end
if (DW < 1) begin : g_bad_dw
$error("DW must be positive");
end
if (AF_MARGIN < 1 || AF_MARGIN > DEPTH) begin : g_bad_af
$error("AF_MARGIN must be in 1..DEPTH");
end
if (AE_MARGIN < 0 || AE_MARGIN >= DEPTH) begin : g_bad_ae
$error("AE_MARGIN must be in 0..DEPTH-1");
end
function automatic logic [AW-1:0] bump_ptr(input logic [AW-1:0] ptr);
if (ptr == DEPTH-1) return '0;
return ptr + 1'b1;
endfunction
assign full_o = (count == DEPTH);
assign empty_o = (count == 0);
assign almost_full_o = (count >= DEPTH - AF_MARGIN);
assign almost_empty_o = (count <= AE_MARGIN);
assign level_o = count;
assign push_take = push_i && !full_o;
assign pop_take = pop_i && !empty_o;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
wr_ptr <= '0;
rd_ptr <= '0;
count <= '0;
dout_o <= '0;
dout_valid_o <= 1'b0;
end else begin
dout_valid_o <= pop_take;
if (push_take) begin
mem[wr_ptr] <= din_i;
wr_ptr <= bump_ptr(wr_ptr);
end
if (pop_take) begin
dout_o <= mem[rd_ptr];
rd_ptr <= bump_ptr(rd_ptr);
end
unique case ({push_take, pop_take})
2'b10: count <= count + 1'b1;
2'b01: count <= count - 1'b1;
default: count <= count;
endcase
end
end
endmodule
The course simulator does not run SVA, so the properties are a snippet. The testbench above checks the same rules procedurally.
Reset deliberately cancels queued words and any uncaptured pop result; the reference counters restart at zero for the new epoch. The two midstream cases check pointers, flags and result-valid directly during reset, then compare fresh data and reject a stale empty pop. A system wrapper must account for cancelled buffered/pending results across its coordinated reset boundary; epoch-local FIFO occupancy alone is not end-to-end delivery conservation.
// snippet: the same rules as SVA properties
module sync_fifo_props #(parameter int DEPTH = 5) (
input logic clk, rst_n, push_i, pop_i, push_take, pop_take,
input logic full_o, empty_o, dout_valid_o,
input logic [$clog2(DEPTH)-1:0] wr_ptr, rd_ptr,
input logic [$clog2(DEPTH+1)-1:0] count
);
assert property (@(posedge clk) disable iff (!rst_n) count <= DEPTH);
assert property (@(posedge clk) disable iff (!rst_n) full_o |-> !empty_o);
assert property (@(posedge clk) disable iff (!rst_n)
push_i && full_o |=> $stable(wr_ptr));
assert property (@(posedge clk) disable iff (!rst_n)
pop_i && empty_o |=> $stable(rd_ptr));
assert property (@(posedge clk) disable iff (!rst_n)
!push_take |=> $stable(wr_ptr));
assert property (@(posedge clk) disable iff (!rst_n)
!pop_take |=> $stable(rd_ptr));
assert property (@(posedge clk) disable iff (!rst_n)
push_take && !pop_take |=> count == $past(count) + 1'b1);
assert property (@(posedge clk) disable iff (!rst_n)
pop_take && !push_take |=> count == $past(count) - 1'b1);
assert property (@(posedge clk) disable iff (!rst_n)
pop_take |=> dout_valid_o);
endmoduleRun the same top with parameter tuples (DW, DEPTH, AF_MARGIN, AE_MARGIN): (8,5,2,1) retains telemetry; (1,2,1,0), (1,3,3,2), (8,16,1,0), (8,16,16,15) cover widths, wrap and threshold limits. Override the top parameters in the simulator rather than editing the reference. Expected-failure guard configurations, run separately, are (8,1,1,0), (0,5,2,1), (8,5,0,1), (8,5,6,1), (8,5,2,-1), (8,5,2,5); each must fail elaboration through the generate-if guards. Random occupancy coverage is checked per configuration and may require additional directed traffic if the finite seed misses a level.
Scenario | Required evidence |
|---|---|
Reset | Empty asserted, full deasserted, level zero, pointers zero, no valid output |
Fill and drain | Every level from 0 through |
Overflow and underflow requests | No pointer, level, or output transaction change |
Simultaneous operations | Partial occupancy holds level; full and empty follow the documented policy |
Pointer wrap | Several wraps with no loss, duplication, or invalid address |
Parameter matrix | Depth 2, 3, 5, 16; width 1 and a normal data width; threshold limits |
Implementation | Expected memory inferred; no reset on array; timing paths and read latency reviewed |
Is the accepted-operation policy identical in RTL, assertions, scoreboard, and integration documentation?
Does the selected memory implementation provide the required read latency and collision behavior?
Are almost thresholds derived from real reaction latency rather than an arbitrary constant?
Have non-power-of-two depths and pointer wrap been tested?
Does downstream logic use dout_valid_o rather than treating held data bits as a transaction?
A long random push/pop run checked by an independent ordered reference queue, provided it also reaches empty, full, simultaneous operations, and multiple pointer wraps. Directed boundary tests ensure those states are not left to chance.
Parameterised bench (default depth 5; directed boundaries, reset epochs, forced pointer wrap, 3000 pseudo-random cycles against a reference queue), run with Icarus Verilog 13.0 (2026-10-16): prints PASS. It says nothing about physical memory inference.
Parameter matrix, run with Icarus Verilog 13.0 (2026-10-16): the five legal tuples print PASS and the six guard tuples fail elaboration as required.
Icarus does not run SVA, so the properties are shown as a snippet and the bench checks the same rules procedurally.