A module intended for bind has one job: observe and judge. It executes inside someone else's design scope, so any drive or side effect becomes an invisible RTL modification.
Inputs only. Every port is an input: no outputs, no inouts, no internal assigns onto port nets. The checker is physically incapable of disturbing the DUT.
No timing influence. No driven delays, no force statements. Assertions, covers, messages, and local bookkeeping registers only.
Parameterized widths. Never hardcode a bus width. Take parameters so one checker binds to every configuration of the target.
Self-contained clocks. Declare default clocking and reset handling inside. The checker must not assume any testbench infrastructure exists.
Named properties. Label every assertion (a_*) and cover (c_*). Labels are the debug handles in waves and reports.
The most reused checker in any environment judges valid-ready stability on a stream port. The table lists its rules; the full module with its testbench sits under Testbench below.
Check | Rule |
|---|---|
|
|
|
|
|
|
|
|
|
|
Watch valid against ready. Slot 3 is the bug the stability rule forbids.
Slot 0: idle, valid 0 and ready 0.
Slot 1: offer, valid 1 with data a5 while ready stays 0.
Slot 2: stall, valid held and data stable at a5.
Slot 3: retraction, valid drops with ready still 0 and data churns to 3c. a_valid_stable and a_data_stable both fire here.
Slot 4: re-offer accepted, valid 1 and ready 1 with data a5.
Slot 5: back-to-back, new data 7e accepted at once.
The liveness bound uses a ranged delay. Icarus 13 cannot parse ranged delays such as ##[1:5]. Verilator 5.048 runs them when the property names its own clock, so the runnable checker below carries the bound in that form.
// snippet
a_ready_bound : assert property (valid && !ready |-> ##[1:MAX_STALL] ready);The bound instance resolves its port map in the target's scope, including signals that never reach the target's ports. Whitebox assertions on FSM state, counters, and grants connect like ports, without exporting them.
// snippet
// Inside arbiter.sv (RTL, unmodified): grant_q and state_q are internal.
// The checker takes them as plain inputs; the bind maps them by name.
module arb_checker #(parameter int N = 4) (
input logic clk, rst_n,
input logic [N-1:0] grant_q,
input logic [1:0] state_q
);
default clocking cb @(posedge clk); endclocking
default disable iff (!rst_n);
a_grant_onehot : assert property ($onehot0(grant_q));
a_gnt_in_gnt : assert property (|grant_q |-> state_q == 2'd2);
endmodule
bind arbiter arb_checker #(.N(REQ_N)) chk (
.clk(clk), .rst_n(rst_n),
.grant_q(grant_q),
.state_q(state_q)
);VISIBILITY: BOUND CHECKER vs TB-SIDE CHECKER
TB-side checker Bound checker
──────────────── ─────────────────────────
sees: DUT ports only sees: ports + ALL internals
path: tb.dut.u_arb. path: resolved by name in
grant_q (fragile target scope (moves
hierarchical ref) with the module)As a parameter. The checker declares DEPTH with a default, and the bind forwards the target's own parameter with #(.DEPTH(DEPTH)).
The instance elaborates inside the RTL scope. An output or an internal drive would modify the design invisibly, bypassing RTL review and possibly synthesis.
The checker, a passthrough link that exposes clock and reset for the bind, and a testbench driving four beats across a 3-cycle stall. The checker carries the ##[1:MAX_STALL] bound, and a stall counter in the testbench cross-checks it.
// engine: verilator
timeunit 1ns; timeprecision 1ps;
// A valid-ready checker bound to a link; the counter shadows the stall bound.
module vr_checker #(
parameter int WIDTH = 8,
parameter int MAX_STALL = 8
) (
input logic clk,
input logic rst_n,
input logic valid,
input logic ready,
input logic [WIDTH-1:0] data
);
default clocking cb @(posedge clk); endclocking
default disable iff (!rst_n);
a_valid_stable : assert property (valid && !ready |=> valid)
else $error("valid dropped before ready");
a_data_stable : assert property (valid && !ready |=> $stable(data))
else $error("data changed during stall");
a_data_known : assert property (valid |-> !$isunknown(data))
else $error("X on data while valid");
// Explicit clock: Verilator 5.048 fails on a ranged delay under default clocking.
a_ready_bound : assert property (@(posedge clk) disable iff (!rst_n)
valid && !ready |-> ##[1:MAX_STALL] ready)
else $error("ready did not arrive within MAX_STALL cycles");
c_b2b : cover property (valid && ready ##1 valid && ready);
endmodule
module axis_stub #(parameter int WIDTH = 8) (
input logic clk,
input logic rst_n,
input logic s_valid,
output logic s_ready,
input logic [WIDTH-1:0] s_data,
output logic m_valid,
input logic m_ready,
output logic [WIDTH-1:0] m_data
);
assign m_valid = s_valid;
assign m_data = s_data;
assign s_ready = m_ready;
endmodule
bind axis_stub vr_checker #(.WIDTH(WIDTH), .MAX_STALL(8)) chk_link (
.clk(clk), .rst_n(rst_n), .valid(m_valid), .ready(m_ready), .data(m_data)
);