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, and the last lesson runs a two-property subset of this checker through a bind.
// 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, count violations in an action block, as the last lesson does.
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 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 Interface and 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.
A green implication whose antecedent never fired checked nothing. The cover turns that silent hole into a number you can read at closure.
almost_full and full separate bins instead of one high-fill bucket?Off-by-one errors live at DEPTH-1 versus DEPTH. A single bucket would report closure while the boundary the bug lives on was never visited.