The checker Construct

Why a dedicated construct for checkers

A real protocol checker is more than one property: it needs auxiliary modeling (a transaction counter, a shadow state machine), several related assertions and covers, shared clock/reset plumbing, and parameters. You can fake this with a module, but modules were designed to synthesize, so they fight you: no sequence/property formal ports, awkward defaults, no free variables. checker ... endchecker is the construct the LRM added for exactly this packaging job — verification-only, instantiable anywhere a concurrent assertion is legal (including inside always blocks), and bind-friendly.

checker req_ack_chk (
  logic req, ack,
  event clk_e = $inferred_clock,           // picks up clock from context
  logic rst   = $inferred_disable          // picks up disable from context
);
  default clocking @clk_e; endclocking
  default disable iff (rst);

  a_hold:    assert property (req && !ack |=> req);
  a_ack_win: assert property ($rose(req) |-> ##[1:8] ack);
  a_no_orph: assert property ($rose(ack) |-> $past(req));
  c_basic:   cover  property ($rose(req) ##[1:8] $rose(ack));
endchecker

// Use: one line per interface instance
req_ack_chk u_chk0 (.req(m0_req), .ack(m0_ack));
req_ack_chk u_chk1 (.req(m1_req), .ack(m1_ack));

$inferred_clock and $inferred_disable let the checker absorb the clock and reset of the instantiation context (for example the enclosing always block or default clocking), so call sites stay one line.

Modeling code and free variables

Checkers may contain variables assigned by procedural code (checker variables) for shadow modeling, and free variables — rand variables that no one assigns. In simulation a free variable takes tool-chosen values; in formal it becomes a nondeterministic input the prover quantifies over. Free variables are how one checker describes "for ANY address a, a write to a followed by a read from a returns the data" without instantiating a checker per address.

checker mem_rdwr_chk #(int AW = 8, DW = 32) (
  logic clk, rst_n, wr, rd,
  logic [AW-1:0] addr,
  logic [DW-1:0] wdata, rdata
);
  default clocking @(posedge clk); endclocking
  default disable iff (!rst_n);

  rand const logic [AW-1:0] watch_addr;    // FREE variable: any address

  // Shadow model only for the watched address — tiny, formal-friendly
  logic [DW-1:0] shadow;
  logic          shadow_valid;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n)                          {shadow_valid, shadow} <= '0;
    else if (wr && addr == watch_addr)   {shadow_valid, shadow} <= {1'b1, wdata};

  a_rd_data: assert property (
    rd && addr == watch_addr && shadow_valid |-> ##1 rdata == shadow);
endchecker

WHY A FREE VARIABLE BEATS A FULL SHADOW MEMORY

  Full shadow memory model            Free-variable watch model
  ─────────────────────────           ─────────────────────────────
  logic [DW-1:0] mem [2**AW];         rand const logic [AW-1:0] watch_addr;
  256+ state elements                 1 register + 1 valid bit
  formal: state explosion             formal: prover picks the WORST addr,
  sim: works, heavy                     proof covers ALL addrs by symmetry
                                      sim: tool picks some addr per run

  "rand const" = chosen once at start, then constant — the standard
  idiom for "for all X" checks in checker libraries.

Defaults, instantiation, and bind

Default clocking and disable inside checkers

A default clocking and default disable iff declared inside the checker apply to every assertion in it — write the clock and reset once instead of per-property. Combined with $inferred_clock/$inferred_disable defaults on the ports, the same checker works whether the context supplies a clock or the instantiation names one explicitly.

Instantiating directly vs binding

• Direct instantiation inside RTL: the designer owns it; checker travels with the code; but it edits the RTL file and ships verification code in design source.

• bind from a separate file: zero RTL edits, DV owns the file, one bind line attaches the checker to every instance of a module type.

• bind target sees the module's internal scope — port connections name internal signals directly.

• Same checker, both flows: write once, let designers instantiate in new code and DV bind onto legacy code.

// bind file (verification-owned, no RTL edits):
bind fifo_core fifo_chk #(.DEPTH(16)) u_fifo_chk (
  .clk    (clk),
  .rst_n  (rst_n),
  .push   (wr_en && !full),
  .pop    (rd_en && !empty),
  .count  (occupancy_q)        // internal signal — visible to bind
);
// Effect: every instance of fifo_core in the design, in every testbench
// that compiles this file, gets the checker — automatically.

The library-of-checkers pattern

Mature teams maintain a directory of parameterized checkers — handshake, FIFO, one-hot arbiter, valid/ready stream, gray-code pointer — each verified once and then bound onto every new design. The payoff compounds: a new block gets hundreds of proven assertions on day one for the cost of a few bind lines.

CHECKER LIBRARY — typical layout and flow

  verif/checkers/
    ├── hs_chk.sv          req/ack + valid/ready handshake rules
    ├── fifo_chk.sv        no overflow/underflow, data integrity, count
    ├── onehot_chk.sv      grant one-hot, fairness window
    ├── stream_chk.sv      valid stable until ready, data stable rule
    └── gray_chk.sv        one-bit-change per clock (async FIFO ptrs)

  new_block.sv  ──┐
                  ├──► binds/new_block_bind.sv:
  fifo_core  x3 ──┤      bind fifo_core  fifo_chk   u_f (...);
  axis_out   x1 ──┘      bind new_block  stream_chk u_s (...);
                                  │
                                  ▼
              every sim AND the formal flow compile the same binds
              → identical checks in both engines, written once

Interview angle

Checker questions usually arrive as methodology probes: "How would you deploy assertions across 30 FIFO instances without editing RTL?" — parameterized checker plus bind is the expected answer; mentioning that bind connections can reach internal signals earns extra credit. The deeper follow-up is free variables: "How do you check ALL addresses without a full shadow memory?" — rand const free variable watching one symbolic address, which formal generalizes to all addresses. If you have only ever put assertions in interfaces, say so honestly, then explain what checker adds: defaults, modeling code, free variables, and legality inside procedural contexts.

Key takeaways

• checker...endchecker packages assertions, covers, and shadow-modeling code into one reusable, bindable unit.

• default clocking / default disable iff inside the checker remove per-property clock/reset boilerplate.

• $inferred_clock/$inferred_disable port defaults absorb clock and reset from the instantiation context.

• rand free variables express for-all checks — one symbolic address instead of a full shadow memory.

• Library-of-checkers + bind gives every new design proven assertions on day one with zero RTL edits.

Common pitfalls

• Building checkers as synthesizable modules — no sequence ports, no free variables, risk of shipping verification logic.

• Re-deriving clock/reset per assertion inside the checker — that is exactly what the defaults exist to remove.

• Full shadow memories in formal-targeted checkers — state explosion; use a free-variable watch model.

• Binding by instance path instead of module type — new instances silently miss the checker.

• Forgetting that checker variables must not be assigned from outside — they are checker-internal state.