Writing Assertion Modules for bind

Conventions for bind-safe modules

A module intended for bind has one job: observe and judge. Its discipline is strict because it executes inside someone else's design scope — any drive, any side effect, becomes an invisible RTL modification.

• Inputs only — every port is input. No output, no inout, no internal continuous assigns onto port nets. The checker must be physically incapable of disturbing the DUT.

• No timing influence — no delays driving anything, no force statements. Assertions, covers, $display/$error and local bookkeeping registers only.

• Parameterized widths — never hardcode bus widths; take parameters so the same checker binds to every configuration of the target.

• Self-contained — default clocking and reset handling declared inside; the checker should not assume any TB infrastructure exists.

• Named assertions — every property gets a label (a_*, c_* for covers) so wave debug and reports identify which check fired.

Worked example: valid/ready handshake checker

The most reused checker in any environment: valid/ready stability rules on a stream port. Written once with parameterized width, bound to every DUT boundary that speaks the protocol.

// vr_checker.sv — bind-safe: inputs only, parameterized
module vr_checker #(
  parameter int WIDTH      = 32,
  parameter int MAX_STALL  = 64      // ready latency bound
) (
  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);

  // valid must hold until accepted
  a_valid_stable : assert property (
    valid && !ready |=> valid
  ) else $error("valid dropped before ready");

  // data must not change while valid is stalled
  a_data_stable : assert property (
    valid && !ready |=> $stable(data)
  ) else $error("data changed during stall");

  // no X on data when valid
  a_data_known : assert property (
    valid |-> !$isunknown(data)
  ) else $error("X/Z on data while valid");

  // liveness bound: ready within MAX_STALL cycles
  a_ready_bound : assert property (
    valid && !ready |-> ##[1:MAX_STALL] ready
  ) else $error("ready exceeded stall bound");

  // coverage: back-to-back accepted beats
  c_b2b : cover property (valid && ready ##1 valid && ready);

endmodule

// Bind it to a DUT output port (in the DV bind file):
bind axis_master vr_checker #(
  .WIDTH (DATA_W),                  // target's own parameter
  .MAX_STALL (64)
) chk_m_axis (
  .clk   (clk),
  .rst_n (rst_n),
  .valid (m_axis_tvalid),
  .ready (m_axis_tready),
  .data  (m_axis_tdata)
);

Walkthrough

1. All five ports are inputs — the checker cannot disturb the handshake it judges.

2. WIDTH comes from the target's DATA_W parameter at bind time — one checker, every bus width.

3. default clocking and default disable iff keep each property one line; reset behavior is uniform.

4. Labels (a_valid_stable, c_b2b) appear in wave viewers and assertion reports — name every property.

Reaching internal signals

Because the bound instance elaborates inside the target, its port map resolves names in the target's scope — including signals that never reach the target's ports. This is bind's superpower over TB-side checking: whitebox assertions on FSM state, counters, and arbitration grants without exporting them.

// Inside arbiter.sv (RTL — unmodified):
//   logic [3:0] grant_q;          // internal one-hot grant register
//   typedef enum logic [1:0] {IDLE, ARB, GNT} state_e;
//   state_e state_q;              // internal FSM state

// Checker takes them as plain inputs:
module arb_checker #(parameter int N = 4) (
  input logic         clk, rst_n,
  input logic [N-1:0] grant_q,     // matched by name in target scope
  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),               // internal regs, visible to bind
  .state_q(state_q)
);

VISIBILITY: BOUND CHECKER vs TB-SIDE CHECKER [DV]

  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)
  breaks on: hierarchy       breaks on: signal rename
        refactor                   inside the module only

Key takeaways

• Bind-safe modules are observers: input ports only, no drives, no timing side effects.

• Parameterize every width and bound; forward the target's parameters in the bind statement.

• Port maps resolve in the target's scope — internal FSM state and counters connect like ports.

• Label every assertion and cover — labels are your debug handles in waves and reports.

Common pitfalls

• An output port or stray continuous assign in the checker — silently drives the DUT through the bind.

• Hardcoded widths — the checker binds to one configuration and silently truncates on others (lint catches it; people don't).

• Referencing internal signals via full hierarchical paths inside the checker instead of ports — defeats reuse and breaks on refactor.

• Unnamed properties — an assertion fires and the report says only the file/line of a checker bound 200 times.