Most assertions are not design-specific. Handshake stability, one-hot encodings, and FIFO occupancy sanity repeat on dozens of interfaces, so each generic check is packaged once as a parameterized, bind-safe module and bound everywhere.
CHECKER LIBRARY — STAMP EVERYWHERE
lib_checkers/ (versioned, project-independent)
┌────────────────────────────────────────────┐
│ chk_handshake #(WIDTH, MAX_STALL) │
│ chk_onehot #(N, ALLOW_ZERO) │
│ chk_fifo #(DEPTH, STRICT_FLAGS) │
│ chk_req_gnt #(MAX_WAIT) │
└────────────────────────────────────────────┘
│ bound via subsystem bind files
▼
dma: 3x handshake, 2x fifo, 1x req-gnt
eth: 5x handshake, 4x fifo, 2x onehot
— zero new assertion code per subsystemLibrary-grade means fully parameterized, single-concern, and severity-controllable, with a header comment stating exactly what is assumed and what is checked. Compose several small binds rather than building one mega-checker.
Both checkers below rely on the default clocking declared inside them. A concurrent assertion with no clocking event and no default clock in scope is illegal, so that declaration is load-bearing, not style.
The FIFO flags carry one documented assumption. Strict definitional equality of full and empty against count holds for a textbook FIFO only, so STRICT_FLAGS gates those two properties for variants like fall-through or almost-full designs.
// engine: verilator
timeunit 1ns; timeprecision 1ps;
// Library pair on one link: one-hot control plus FIFO occupancy.
module chk_onehot #(
parameter int N = 4,
parameter bit ALLOW_ZERO = 1
) (
input logic clk,
input logic rst_n,
input logic [N-1:0] vec
);
default clocking cb @(posedge clk); endclocking
default disable iff (!rst_n);
generate
if (ALLOW_ZERO) begin : g_oh0
a_onehot0 : assert property ($onehot0(vec))
else $error("vector is not one-hot-0");
end else begin : g_oh
a_onehot : assert property ($onehot(vec))
else $error("vector is not one-hot");
end
endgenerate
endmodule
module chk_fifo #(
parameter int DEPTH = 8,
parameter bit STRICT_FLAGS = 1
) (
input logic clk, rst_n,
input logic push, pop, full, empty,
input logic [$clog2(DEPTH):0] count
);
default clocking cb @(posedge clk); endclocking
default disable iff (!rst_n);
a_no_push_full : assert property (full |-> !push || pop)
else $error("push into full fifo");
a_no_pop_empty : assert property (empty |-> !pop)
else $error("pop from empty fifo");
a_count_range : assert property (count <= DEPTH);
generate
if (STRICT_FLAGS) begin : g_strict
a_full_def : assert property (full == (count == DEPTH));
a_empty_def : assert property (empty == (count == 0));
end
endgenerate
endmodule
module ctrl_stub (
input logic clk, rst_n,
input logic [3:0] vec
);
endmodule
module mini_fifo #(parameter int DEPTH = 8) (
input logic clk, rst_n,
input logic push, pop,
output logic full, empty,
output logic [$clog2(DEPTH):0] count
);
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) count <= '0;
else case ({push && !full, pop && !empty})
2'b10: count <= count + 1'b1;
2'b01: count <= count - 1'b1;
default: count <= count;
endcase
end
assign full = (count == DEPTH);
assign empty = (count == '0);
endmodule
bind ctrl_stub chk_onehot #(.N(4), .ALLOW_ZERO(1)) chk_oh (
.clk(clk), .rst_n(rst_n), .vec(vec)
);
bind mini_fifo chk_fifo #(.DEPTH(DEPTH), .STRICT_FLAGS(1)) chk_occ (
.clk(clk), .rst_n(rst_n), .push(push), .pop(pop),
.full(full), .empty(empty), .count(count)
);
SystemVerilog also offers a dedicated checker block: verification-only, compiler-enforced no-drive discipline, and bindable like a module. Unlike modules, checkers take no #() parameter list: constants arrive as formal arguments. Many teams stay with plain modules for portability and reach for checkers where the enforced discipline pays off.
The full treatment, including clock inference and free variables, lives in the SVA topic. The listing below is not run in this course's checks: Icarus 13 has no checker support, and Verilator 5.048 rejects the port default and stops with an internal error on the ranged delay.
// not-run: Icarus 13 has no checker support; Verilator 5.048 rejects the port default and hits an internal error on ##[1:MAX_WAIT]
// No #() list: MAX_WAIT is a formal argument bound to a constant.
checker chk_gnt_after_req (
input logic clk, rst_n, req, gnt,
input int MAX_WAIT = 16
);
default clocking @(posedge clk); endclocking
default disable iff (!rst_n);
a_gnt_bound : assert property (
$rose(req) |-> ##[1:MAX_WAIT] gnt
) else $error("grant exceeded wait bound");
endchecker
// bound like a module, with the constant passed as an argument:
bind arbiter chk_gnt_after_req chk_rg (
.clk(clk), .rst_n(rst_n), .req(req0), .gnt(gnt0), .MAX_WAIT(16));The library is its own repo with semantic-version tags, and projects pin a tag, never head. Changing a shipped checker's behavior is a major version bump, because it can flip regressions in every consuming project.
Each release ships a self-test bench: tiny stubs that intentionally violate each assertion, proving every check still fires. A project that needs a tweak parameterizes or contributes the option upstream behind a default-off parameter.
The runnable shadow of that self-test idea: a manual one-hot monitor in plain Verilog injects three illegal vectors and must flag exactly those three. No concurrent assertions are involved, so the violation traffic itself is the stimulus.
timeunit 1ns; timeprecision 1ps;
module tb_onehot_selftest;
reg [3:0] vec = 4'b0000;
integer flagged = 0;
integer errors = 0;
always @(vec) begin
if ((vec & (vec - 4'd1)) !== 4'b0000) flagged = flagged + 1;
end
initial begin
#1 vec = 4'b0001;
#1 vec = 4'b0010;
#1 vec = 4'b0011;
#1 vec = 4'b0100;
#1 vec = 4'b1100;
#1 vec = 4'b0000;
#1 vec = 4'b1111;
#1 vec = 4'b1000;
#1;
if (flagged !== 3) errors = errors + 1;
if (errors == 0) $display("PASS: manual one-hot monitor flagged all 3 injected violations");
else $fatal(1, "FAIL: one-hot self-test flagged %0d of 3 injected violations", flagged);
$finish;
end
endmoduleSTRICT_FLAGS to 0?When its flags are not definitional: fall-through latency, almost-full or almost-empty thresholds, or read-latency variants where full need not equal count == DEPTH.
Treat it as a major bump. Labels are the library's public handles: $assertoff paths, waiver files and triage scripts key on them, so a rename can break consumers even though no check changes.