The checker is a separate module attached with bind. The RTL is never edited, and the checker rides along to every level where the FIFO instantiates.
The module below is not run in this course's checks. It is a checker plus a bind with no testbench, and the course's Verilator 5.048 cannot compile its local-variable data property. The other properties and covers compile under verilator --assert.
// not-run: fragment: checker and bind with no testbench top; Verilator 5.048 also cannot compile the local-variable property
module fifo_sva #(parameter int WIDTH = 8, parameter int DEPTH = 16) (
input logic clk, rst_n,
input logic in_valid, in_ready,
input logic [WIDTH-1:0] in_data,
input logic out_valid, out_ready,
input logic [WIDTH-1:0] out_data,
input logic full, empty
);
wire push = in_valid && in_ready;
wire pop = out_valid && out_ready;
// independent occupancy model
int count;
always_ff @(posedge clk or negedge rst_n)
if (!rst_n) count <= 0;
else count <= count + (push && !pop) - (pop && !push);
default clocking cb @(posedge clk); endclocking
default disable iff (!rst_n);
// F-04: flag mirrors. These sample preponed values: if the combinational
// flags settle late, prove them with the procedural mirror in Testbench.
a_ready_def: assert property (in_ready == !full);
a_valid_def: assert property (out_valid == !empty);
// F-02/F-03: flags exactly track the model count
a_full_def: assert property (full == (count == DEPTH));
a_empty_def: assert property (empty == (count == 0));
// F-05/F-06: boundary protection
a_no_push_full: assert property (full |-> !push);
a_no_pop_empty: assert property (empty |-> !pop);
c_full_seen: cover property (full); // each boundary antecedent occurred
c_empty_seen: cover property (empty);
// count stays in range — catches model/DUT divergence immediately
a_count_range: assert property (count inside {[0:DEPTH]});
// F-01: data integrity with a local variable — a word pushed into an
// empty FIFO must come out unmodified on the FIRST pop after it. No
// time bound: consumer stalls are legal (F-10). Full in-order checking
// across all fill levels is the scoreboard's job.
property p_data_integ_empty;
logic [WIDTH-1:0] d;
(push && empty, d = in_data)
|=> pop[->1] ##0 (out_data == d);
endproperty
a_data_integ_empty: assert property (p_data_integ_empty);
c_data_integ_ante: cover property (push && empty);
// corner hooks for F-07/F-08, each paired with the assertion that checks it
c_simul: cover property (push && pop);
c_simul_full: cover property (full && pop && in_valid);
endmodule
// in tb_top or a bind file — attach to EVERY fifo instance:
bind fifo fifo_sva #(.WIDTH(WIDTH), .DEPTH(DEPTH)) u_sva (
.clk(clk), .rst_n(rst_n),
.in_valid(in_valid), .in_ready(in_ready), .in_data(in_data),
.out_valid(out_valid), .out_ready(out_ready), .out_data(out_data),
.full(full), .empty(empty)
);The independent count cross-checks the DUT against the spec, not against itself.
Every implication carries a cover on its antecedent, so no pass is vacuous-only.
The data property checks the first pop after the push, with no time bound, because consumer stalls are legal (F-10). A fixed window would fire on a legal 16-cycle stall. Each push into an empty FIFO starts one attempt, so attempts stay few.
The same flag checks as procedural code. This runnable subset mirrors the occupancy independently and checks every flag each cycle.
module fifo4 (
input logic clk,
input logic rst_n,
input logic in_valid,
output logic in_ready,
input logic [7:0] in_data,
output logic out_valid,
input logic out_ready,
output logic [7:0] out_data,
output logic full,
output logic empty
);
localparam int DEPTH = 4;
logic [7:0] mem [DEPTH];
logic [1:0] wr_ptr = 2'd0, rd_ptr = 2'd0;
logic [2:0] count = 3'd0;
wire push = in_valid && in_ready;
wire pop = out_valid && out_ready;
assign full = (count == 3'd4);
assign empty = (count == 3'd0);
assign in_ready = !full;
assign out_valid = !empty;
assign out_data = mem[rd_ptr];
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
count <= 3'd0;
wr_ptr <= 2'd0;
rd_ptr <= 2'd0;
end else begin
if (push) mem[wr_ptr] <= in_data;
if (push) wr_ptr <= wr_ptr + 2'd1;
if (pop) rd_ptr <= rd_ptr + 2'd1;
if (push && !pop) count <= count + 3'd1;
else if (pop && !push) count <= count - 3'd1;
end
end
endmodule
The covergroup below is a class that needs fifo_if, with no top module, so this course's checks do not run it.
// not-run: fragment: needs fifo_if from the harness lesson and has no top module
class fifo_cov #(parameter int WIDTH = 8, parameter int DEPTH = 16);
virtual fifo_if #(WIDTH) vif;
int count; // mirror of occupancy before this edge's op
covergroup cg_big; // no clocking event: run() calls sample()
option.per_instance = 1;
option.cross_auto_bin = 0; // only the explicit cross bins below count
cp_count: coverpoint count {
bins empty = {0};
bins one = {1};
bins mid = {[2:DEPTH-2]};
bins almost_full = {DEPTH-1};
bins full = {DEPTH};
}
cp_op: coverpoint {vif.mon_cb.in_valid && vif.mon_cb.in_ready,
vif.mon_cb.out_valid && vif.mon_cb.out_ready} {
bins idle = {2'b00};
bins push = {2'b10};
bins pop = {2'b01};
bins both = {2'b11};
}
cp_flags: coverpoint {vif.mon_cb.full, vif.mon_cb.empty} {
bins normal = {2'b00};
bins full_ = {2'b10};
bins empty_ = {2'b01};
illegal_bins both_flags = {2'b11};
}
x_op_state: cross cp_op, cp_count {
bins push_at_almost_full = binsof(cp_op.push) && binsof(cp_count.almost_full);
bins pop_to_empty = binsof(cp_op.pop) && binsof(cp_count.one);
bins both_mid = binsof(cp_op.both) && binsof(cp_count.mid);
}
// F-08: a pop at full with a push offered (in_ready low blocks it)
cp_offer_at_full: coverpoint
(vif.mon_cb.full && vif.mon_cb.in_valid && vif.mon_cb.out_ready) {
bins seen = {1};
}
cp_backpressure: coverpoint
(vif.mon_cb.full && vif.mon_cb.in_valid && !vif.mon_cb.out_ready) {
bins seen = {1};
}
endgroup
// small-DEPTH covergroup: at DEPTH 2..3 the mid range is empty and
// almost_full collides with one, so those bins do not exist here
covergroup cg_small;
option.per_instance = 1;
option.cross_auto_bin = 0;
cp_count: coverpoint count {
bins empty = {0};
bins one = {1};
bins full = {DEPTH};
}
cp_op: coverpoint {vif.mon_cb.in_valid && vif.mon_cb.in_ready,
vif.mon_cb.out_valid && vif.mon_cb.out_ready} {
bins idle = {2'b00};
bins push = {2'b10};
bins pop = {2'b01};
bins both = {2'b11};
}
cp_flags: coverpoint {vif.mon_cb.full, vif.mon_cb.empty} {
bins normal = {2'b00};
bins full_ = {2'b10};
bins empty_ = {2'b01};
illegal_bins both_flags = {2'b11};
}
x_op_state: cross cp_op, cp_count {
bins pop_to_empty = binsof(cp_op.pop) && binsof(cp_count.one);
}
cp_offer_at_full: coverpoint
(vif.mon_cb.full && vif.mon_cb.in_valid && vif.mon_cb.out_ready) {
bins seen = {1};
}
cp_backpressure: coverpoint
(vif.mon_cb.full && vif.mon_cb.in_valid && !vif.mon_cb.out_ready) {
bins seen = {1};
}
endgroup
function new(virtual fifo_if #(WIDTH) v);
vif = v;
if (DEPTH > 3) cg_big = new(); // only one instance ever samples
else cg_small = new();
endfunction
// One process orders everything: sample with the count BEFORE this
// edge's op, then update the mirror. No second process races it.
task run();
forever begin
@(vif.mon_cb);
if (!vif.rst_n) begin
count = 0;
continue; // no sampling during reset
end
if (cg_big != null) cg_big.sample();
else cg_small.sample();
count += (vif.mon_cb.in_valid && vif.mon_cb.in_ready)
- (vif.mon_cb.out_valid && vif.mon_cb.out_ready);
end
endtask
endclassBoundary bins stay separate. A mid-range bucket hiding DEPTH-1 would fake closure on the off-by-one zone.
The cross holds only explicit bins. Auto-bins would dilute the closure claim with uninteresting combinations.
Sampling is explicit and gated by reset. run() calls sample() after the clocking event and before it updates the mirror, so each bin pairs the op at this edge with the count before it. A covergroup clocked on the same edge as the mirror update would race it.
Watch count, full and empty. Slot 5 holds full with the producer still offering, and slots 6 to 7 drain.
Slot 0: reset: count 0, empty 1.
Slot 1: push: count 1, empty 0.
Slot 2: push: count 2.
Slot 3: push: count 3.
Slot 4: push: count 4, full 1.
Slot 5: producer still offers while full: the push is ignored, count pinned at 4.
Slot 6: pop drains to 3, full falls.
Slot 7: drain continues to 2.
One environment, many tests. Each test is a thin recipe over scenarios, knobs and length, mapping straight back to plan rows.
TEST VARIANTS
Test │ Recipe │ Plan rows
────────────────┼─────────────────────────────────────┼───────────────
smoke │ 20 pushes, 20 pops, fixed seed │ F-01,04 (sanity)
stress_mixed │ 2000 txns SCN_MIXED, max_gap 0-1 │ F-01,07, wrap
burst_drain │ fill→full, hold, drain→empty, x10 │ F-02,03,05,06,10
corner_simul │ park at full / at empty, OP_BOTH │ F-07,08
reset_storm │ random resets mid-traffic, restart │ F-09
error_probe │ in_valid at full, out_ready at │ F-05,06
│ empty held for windows │
param_min │ rebuild DEPTH=2, run all the above │ F-11
param_w1 │ rebuild WIDTH=1, smoke + stress │ F-11// snippet: a test is a recipe over the generator and scoreboard above
task test_burst_drain(generator #(8) gen, fifo_sb #(8) sb);
repeat (10) begin
gen.run_scenario(SCN_BURST_FILL, 24); // past DEPTH: park at full
gen.run_scenario(SCN_BACKPRESSURE, 10); // hold full under pressure
gen.run_scenario(SCN_DRAIN, 24); // past DEPTH: park at empty
end
endtaskREGRESSION TIERS
per-checkin smoke + 1 seed of stress_mixed ~2 min
nightly all tests x 10 seeds x {DEPTH=16} ~1 hr
+ param_min, param_w1 x 3 seeds
weekly soak stress_mixed x 200 seeds, reset_storm coverage
x 50 seeds, merge ALL coverage closure run
bookkeeping per run: seed, test, RTL version, pass/fail, ucdb path
→ failures reproducible with one command; coverage merge automaticEvery uncovered bin gets a written disposition after the soak merge. Three findings are typical.
cp_offer_at_full at 0 hits: the generator never offered a push during a pop while parked at full. Fix: corner_simul parks at full, then issues OP_BOTH bursts. Re-run covered it, and a_no_push_full exposed a real RTL bug: in_ready rose at full whenever out_ready was high, so a push was accepted at full, against Q-003.
cp_count.almost_full thin in 200 seeds: mixed traffic crosses the boundary too fast. Fix: SCN_BACKPRESSURE weight raised in stress_mixed. Now hundreds of hits.
param_w1 by reset_storm uncovered nothing new after 3 seeds. Waiver: WIDTH 1 has no width-dependent reset logic. Documented, approved, closed.
Sign-off is an evidence bundle, not a feeling. Plan closure, merged coverage, assertion health, scoreboard volume and a converged bug rate each contribute one line.
SIGN-OFF SUMMARY — fifo v1.2 (example of the bundle)
plan rows 11/11 closed (10 covered+checked, 1 waived: F-11/W1 note)
functional coverage 17/17 bins hit after merge (illegal_bins excluded by design)
assertions 8 properties, 0 failures final regression,
every antecedent cover hit (no vacuous-only passes)
scoreboard every word compared across the soak, 0 differences
bugs found 3 RTL (incl. push accepted at full), 2 TB, all closed
bug-rate 0 new bugs in final 2 weekly soaks
residual risk async use unverified (out of scope: sync FIFO only)A directed fix, not a waiver. Park at full, issue OP_BOTH bursts, re-run to cover. The gap once exposed a real RTL bug: a push accepted at full during a pop.
No. Closure needs the merged soak across seeds and configs. One seed proves the mechanisms run, not that the corners are covered.