Most blocks on a chip speak a handful of protocols. If each designer writes their own valid/ready assertions, the same rule exists in thirty versions, half of them with a subtle error. A library writes each rule once, tests it once, and binds it everywhere. The pieces are let for Boolean helpers, parameterized properties for the temporal rules, and a module or checker that packages them with bind.
Need | text macro (define) | function | let |
|---|---|---|---|
Scope | Global from the point of definition | Normal scoping | Normal scoping; can live in a package |
Usable in assertions | Yes (text) | Yes, with limits | Yes, it is an expression template |
What it is | Text pasted before parsing | A call evaluated at run time | An expression template expanded where it is used |
Arguments | Untyped text | Typed | Typed or untyped, with defaults |
Shows up in the debugger | No | Yes | Yes |
The LRM says let can replace text macros in many cases and that putting let declarations in packages is the natural way to share them. A let is expanded where it is used, so let moved(x) = !$stable(x); samples x on the clock of the assertion that uses it.
// snippet: let helpers. One definition, used in assertions and in procedural code.
package hs_lib_pkg;
let stalled(v, r) = v && !r;
let fired(v, r) = v && r;
let in_range(x, lo, hi) = (x >= lo) && (x <= hi);
endpackageA named sequence or property with formal arguments is a template. The formal can be typed (logic v), untyped, or a sequence or property itself, which lets a library pass a whole sub-property in. A library property should take every signal as an argument; one that names module signals directly cannot be reused.
Tool support for the flexible parts varies. Verilator 5.048 rejected a property formal with a default value ("Unsupported: property variable default value") and rejected an untyped formal passed to $rose ("Expected numeric type, but got a 'untyped' data type"). Typed formals worked. The library below therefore types its formals and gets width flexibility from a module parameter instead.
SystemVerilog has a construct made for this: checker (Clause 17). A checker can take untyped formals, hold free variables for formal tools and be instantiated inside procedural code. A parameterized module bound with bind does most of the same job and is supported everywhere. In our test, Verilator 5.048 compiled a checker with an untyped data formal, but a change confined to bit 8 of a 16-bit signal was not seen, so the formal behaved narrower than the signal. This lesson uses a module. If your tools handle checkers fully, the same structure moves into a checker unchanged.
The bench below holds one package, one checker module and two unrelated sources: an 8-bit packet source whose payload must stay in 0..199, and a 16-bit counter source with no range limit. One bind line per DUT sets the width and range. The checker counts failures and activity, so the test can prove the run was not vacuous.
// ---- Library: one package of let helpers, one parameterized checker ----
package hs_lib_pkg;
let stalled(v, r) = v && !r;
let fired(v, r) = v && r;
let in_range(x, lo, hi) = (x >= lo) && (x <= hi);
endpackage
module hs_checker #(
parameter int W = 8,
parameter logic [W-1:0] LO = '0,
parameter logic [W-1:0] HI = '1
) (
input logic clk,
input logic rst_n,
input logic valid,
input logic ready,
input logic [W-1:0] data
);
import hs_lib_pkg::*;
int unsigned fails = 0, n_stall = 0, n_fire = 0;
// Parameterized properties: the ports make them reusable inside the library.
property p_hold(logic v, logic r, logic [W-1:0] d);
@(posedge clk) disable iff (!rst_n)
stalled(v, r) |=> v && $stable(d);
endproperty
property p_legal(logic v, logic [W-1:0] d);
@(posedge clk) disable iff (!rst_n)
v |-> in_range(d, LO, HI);
endproperty
a_hold: assert property (p_hold(valid, ready, data)) else fails++;
a_legal: assert property (p_legal(valid, data)) else fails++;
c_stall: cover property (@(posedge clk) disable iff (!rst_n) stalled(valid, ready));
// The same let helpers work in procedural code: here they count activity.
always @(posedge clk) if (rst_n) begin
if (stalled(valid, ready)) n_stall++;
if (fired(valid, ready)) n_fire++;
end
endmodule
// ---- Two different DUTs with a valid/ready output ----
module pkt_src (
input logic clk, rst_n, en, out_ready,
output logic out_valid,
output logic [7:0] out_data
);
always_ff @(posedge clk) begin
if (!rst_n) begin
out_valid <= 0;
out_data <= 0;
end else if (!out_valid || out_ready) begin
out_valid <= en;
if (en) out_data <= (out_data == 8'd199) ? 8'd0 : out_data + 1; // payload 0..199
end
end
endmodule
module cnt_src (
input logic clk, rst_n, en, ready,
output logic valid,
output logic [15:0] count
);
always_ff @(posedge clk) begin
if (!rst_n) begin
valid <= 0;
count <= 0;
end else if (!valid || ready) begin
valid <= en;
if (en) count <= count + 16'd3;
end
end
endmodule
// ---- One bind per DUT: same library, different widths and ranges ----
bind pkt_src hs_checker #(.W(8), .LO(8'd0), .HI(8'd199)) u_hs (
.clk, .rst_n, .valid(out_valid), .ready(out_ready), .data(out_data));
bind cnt_src hs_checker #(.W(16)) u_hs (
.clk, .rst_n, .valid(valid), .ready(ready), .data(count));
Two mutants show that each binding works on its own DUT. Making cnt_src add 16'h100 while stalled, so only the upper byte moves, gives 512 failures on cnt_src and none on pkt_src; this also proves the full 16 bits reach the checker. Making pkt_src wrap at 255 instead of 199 gives 319 range failures on pkt_src only.
Clock and reset are ports, and every property carries its own disable iff, so the library never depends on the bind site.
Limits are parameters with safe defaults (HI = '1 means no range check).
Every assertion has a label. Reports name the label, and assertion control tasks select by it.
The checker counts its own activity (stalls and transfers here). A library that cannot show it was exercised cannot be signed off.
Bind statements live in one bind file per block, outside the RTL, so designers never edit them.
For formal reuse, add a parameter that turns input-side rules into assumptions (see the formal lesson).
stalled(v, r)?A let has normal scoping, so two packages can define different stalled helpers without clashing, it can be imported from a package, it appears in the debugger, and its arguments are evaluated as expressions rather than pasted as text.
That the checker sees fewer than 16 bits of data, for example because a formal was too narrow or untyped and truncated. The mutant is chosen to catch that, not only the DUT bug.