Checkers

Module 17 · Page 17.3

A checker is a dedicated SystemVerilog construct (checker … endchecker, IEEE 1800-2017 §17) that packages assertions, sequences, properties, coverage, and helper logic into one named, reusable unit. It looks almost like a module, but it is built for verification: its variables are automatic per-instance, it supports default clocking and default disable iff so you write the clock and reset condition once, and it supports free variables for formal verification. You instantiate it like a module — inside a design block, inside an interface, or non-invasively via bind (the previous lesson). This page covers what a checker may contain, the declaration and instantiation forms, a complete AHB-Lite protocol checker, free variables, and exactly when to reach for checker instead of module.

1. Engineering Problem — Assertions Need a Home

Once a block has more than a handful of assertions, writing them loose inside the RTL (or scattered across the testbench) breaks down:

• Boilerplate repeats. Every assert property needs @(posedge clk) and disable iff (!rst_n). Twenty properties means twenty copies of the same clock and reset text — and one forgotten disable iff fires spuriously during reset.
• No reuse. The same protocol rules (AHB, APB, AXI) get re-typed for every block instead of dropped in as a unit.
• Namespace clashes. A property p_valid here collides with a property p_valid there when they live in the same scope.
• No per-instance isolation. A module-as-checker has static variables by default — instantiate it twice and a shared counter silently corrupts across instances.
• No formal story. Pure-simulation assertions don't give a formal tool the universally-quantified properties it needs to prove correctness for all values.

The checker construct solves all of these at once: one container, one default clocking, one default disable iff, scoped sequence/property names, automatic per-instance variables, and free variables for formal — instantiable anywhere, including via bind onto RTL you don't own.

2. Mental Model — A Named, Reusable Verification Container

The picture every engineer carries:

A checker is a module-shaped box that holds verification, not hardware. Swap module/endmodule for checker/endchecker and you get a unit whose ports are observe-only (input/output, never inout), whose local variables are automatic (each instance independent), and which understands default clocking and default disable iff so the clock and reset condition are declared once for every property inside. You instantiate it like a module — directly in a design block, inside an interface, or via bind — and it sees exactly the signals wired to its ports, nothing hierarchically above.

Four invariants this picture preserves:

• Verification-only. A checker holds assertions, coverage, and helper tracking logic — never synthesizable design logic. Synthesis ignores it.
• Automatic by default. Local variables are per-instance, so binding one checker to ten FIFOs gives ten independent counters — no shared static state.
• Write clock/reset once. default clocking and default disable iff apply to every concurrent assertion in the body, eliminating the per-property boilerplate that causes reset-time false failures.
• rand means free variable, not stimulus. Inside a checker, rand declares a formal free variable (universally quantified by a formal tool) — fundamentally different from rand in a class.

3. Visual Explanation — Where a Checker Attaches

One checker, three instantiation contexts. The same checker unit drops into a design block, lives inside an interface so every user inherits it, or attaches non-invasively through bind.

What a checker body may contain (IEEE 1800-2017 §17):

4. Declaring a checker

The syntax mirrors a module — swap module/endmodule for checker/endchecker.

checker my_checker (input logic clk, rst_n, valid, data);
 
    // default clocking — every property below uses posedge clk unless overridden
    default clocking cb @(posedge clk); endclocking
 
    // default reset — every concurrent assertion disables during reset
    default disable iff (!rst_n);
 
    // local variable — automatic: each instance gets its own copy
    int valid_count = 0;
 
    // named sequence — scoped to this checker
    sequence s_valid_data;
        valid ##1 data;
    endsequence
 
    // named property
    property p_data_follows_valid;
        valid |-> ##1 !$isunknown(data);
    endproperty
 
    // labelled assertion — the label appears in logs / waveforms / formal reports
    data_valid_chk: assert property (p_data_follows_valid)
        else $error("data is X/Z one cycle after valid!");
 
    // coverage
    cov_valid_seen: cover property (s_valid_data);
 
    // helper tracking logic — clocked here; bare `always` defaults to always_comb
    always @(posedge clk)
        if (valid) valid_count++;
 
endchecker   // ← endchecker, not endmodule

Reading it: checker declares the verification unit (the compiler applies checker rules — no inout, automatic variables); the port list is the only window into the instantiation context (a checker cannot reach parent signals hierarchically); default clocking and default disable iff apply body-wide; sequence/property names are scoped to the checker; and every assert/cover should carry a label so a failure names the rule, not just a file and line.

5. Instantiating a checker

A checker instantiates like a module — named, positional, or .* connections — and can live in a design block, an interface, or be attached via bind.

// ── Context 1 — directly inside a design block ──────────────────────
module ahb_master (input logic hclk, hresetn, hready, output logic [1:0] htrans);
    // ... RTL ...
    ahb_chk u_ahb_chk (.clk(hclk), .rst_n(hresetn), .hready(hready), .htrans(htrans));
    // or, if checker port names match the signal names:  ahb_chk u_ahb_chk (.*);
endmodule
 
// ── Context 2 — via bind (non-invasive, separate file) ──────────────
bind ahb_master  ahb_chk u_ahb_chk (
    .clk(hclk), .rst_n(hresetn), .hready(hready), .htrans(htrans)
);
 
// ── Context 3 — inside an interface (every user inherits the checker) ─
interface ahb_if (input logic hclk, hresetn);
    logic [1:0] htrans;
    logic       hready;
    ahb_chk u_chk (.clk(hclk), .rst_n(hresetn), .hready(hready), .htrans(htrans));
endinterface

The bind form (Context 2) is the production best practice for IP verification: a reusable checker unit attached without editing the RTL — the two Module 17 mechanisms compose directly.

6. Full Working Example — AHB-Lite Protocol Checker

A real protocol checker for the AHB-Lite bus, enforcing three rules. Note how the single default clocking and default disable iff keep every property clean.

checker ahb_lite_chk (
    input logic        hclk,      // bus clock
    input logic        hresetn,   // active-low reset
    input logic [1:0]  htrans,    // transfer type: IDLE/BUSY/NONSEQ/SEQ
    input logic [2:0]  hburst,    // burst type
    input logic        hready,    // slave ready
    input logic [31:0] haddr,     // address
    input logic        hwrite     // 1 = write, 0 = read
);
    localparam logic [1:0] IDLE = 2'b00, BUSY = 2'b01, NONSEQ = 2'b10, SEQ = 2'b11;
 
    default clocking ahb_cb @(posedge hclk); endclocking
    default disable iff (!hresetn);
 
    // Rule 1 — a NONSEQ held during a wait state must stay NONSEQ or become SEQ
    property p_nonseq_hold;
        (htrans == NONSEQ && !hready) |=> (htrans inside {NONSEQ, SEQ});
    endproperty
    nonseq_hold_chk: assert property (p_nonseq_hold)
        else $error("AHB Protocol Violation: NONSEQ not held when hready=0");
 
    // Rule 2 — BUSY is illegal immediately after IDLE (BUSY is a mid-burst state)
    property p_no_busy_after_idle;
        (htrans == IDLE) |=> (htrans != BUSY);
    endproperty
    busy_after_idle_chk: assert property (p_no_busy_after_idle)
        else $error("AHB Protocol Violation: BUSY seen immediately after IDLE");
 
    // Rule 3 — address must be stable while hready is de-asserted
    property p_addr_stable;
        (htrans != IDLE && !hready) |=> $stable(haddr);
    endproperty
    addr_stable_chk: assert property (p_addr_stable)
        else $error("AHB Protocol Violation: haddr changed while hready=0");
 
    // Coverage — was every transfer type exercised?
    cov_idle:   cover property (htrans == IDLE);
    cov_nonseq: cover property (htrans == NONSEQ);
    cov_seq:    cover property (htrans == SEQ);
    cov_busy:   cover property (htrans == BUSY);
    cov_write:  cover property (htrans == NONSEQ && hwrite);
    cov_read:   cover property (htrans == NONSEQ && !hwrite);
endchecker

// Attach it — one line, zero RTL impact (.* matches ports to signal names)
module ahb_master (
    input  logic        hclk, hresetn, hready,
    output logic [1:0]  htrans,
    output logic [2:0]  hburst,
    output logic [31:0] haddr,
    output logic        hwrite
);
    // ... RTL logic ...
    ahb_lite_chk u_ahb_chk (.*);
endmodule

$ xrun ahb_master.sv ahb_lite_chk.sv tb_ahb.sv -sv
Elaboration complete. Running simulation...
 
ERROR: AHB Protocol Violation: NONSEQ not held when hready=0
       File: ahb_lite_chk.sv  Time: 520ns  Assertion: nonseq_hold_chk
       Instance: top.u_dut.u_ahb_chk
 
Coverage Report:
  cov_idle   — hit 42 times
  cov_nonseq — hit 18 times
  cov_seq    — hit 7 times
  cov_busy   — NEVER HIT (0 times)  ← coverage hole

7. Free Variables — For Formal Verification

A checker-exclusive feature with no module equivalent. A free variable is a variable declared rand inside a checker. In simulation it takes a random value; in a formal tool it is universally quantified — the tool considers every possible value at once. That lets one property say "for any data value, if it is written it must eventually appear at the output," without enumerating values.

checker fifo_data_integrity (
    input logic       clk, rst_n,
    input logic       wr_en, rd_en,
    input logic [7:0] din, dout,
    input logic       full, empty
);
    default clocking cb @(posedge clk); endclocking
    default disable iff (!rst_n);
 
    // Free variable — formal considers ALL 8-bit values; sim picks one at random
    rand logic [7:0] ref_data;
 
    // If ref_data is written, it must eventually be read back out unchanged
    property p_data_preserved;
        (wr_en && !full && (din == ref_data))
        |-> strong(##[1:$] (rd_en && !empty && (dout == ref_data)));
    endproperty
    data_preserved_chk: assert property (p_data_preserved)
        else $error("FIFO data integrity violation: written data not seen at output");
endchecker

8. checker vs module — Which to Use

Both can hold assertions; the checker construct is purpose-built for it.

9. Industry Usage — Where Checkers Show Up

• Reusable protocol-checker libraries — AHB/APB/AXI/SPI decks shipped as checker units, bound onto every bus instance.
• Formal sign-off — checkers with free variables and assume property are the natural unit a formal tool targets for end-to-end proofs.
• Interface-embedded checkers — a checker inside an interface so every block that uses the interface inherits the protocol checks automatically.
• Coverage decks — cover property collections that report holes back to the testbench (the BUSY example) as a verification to-do list.
• UVM environments — checkers bound onto the DUT complement class-based scoreboards with cycle-accurate temporal checks the scoreboard can't easily express.

10. Debugging Guide — The Mistakes Everyone Makes Once

checker my_chk (inout logic data);   // ❌ illegal

default clocking cb @(posedge clk); endclocking
// ❌ no default disable iff — every assertion fires during reset

checker c(...); rand logic [7:0] pkt_data; ... endchecker  // free variable, not stimulus

11. Q & A

12. Cross-References & What's Next

This lesson covered the checker construct — its contents, automatic semantics, default clocking/disable iff, free variables, the three instantiation contexts, and checker vs module.

• Previous: 17.2 — The bind Construct — the non-invasive way to attach a checker to RTL you don't own; checkers and bind compose directly.
• Module index: Module 17 — Advanced Topics — the advanced-feature arc.

Related material elsewhere in the curriculum:

• Concurrent Assertions — the property/sequence machinery a checker packages.
• Intro to SVA — assertion fundamentals; a checker is where a reusable assertion deck lives.

13. Quick Reference

// ── Declare a checker ───────────────────────────────────────────────
checker my_chk (input logic clk, rst_n, sig_a, sig_b);
 
    default clocking cb @(posedge clk); endclocking   // write clock once
    default disable iff (!rst_n);                      // write reset once
 
    int count = 0;                  // automatic — per instance
    rand logic [7:0] free_val;      // FREE VARIABLE (formal), not CRV stimulus
 
    sequence s_handshake; sig_a ##1 sig_b; endsequence
    property p_b_follows_a; sig_a |-> ##[1:3] sig_b; endproperty
 
    b_follows_a: assert property (p_b_follows_a)   // ALWAYS label
        else $error("sig_b did not follow sig_a within 3 cycles");
    cov_handshake: cover property (s_handshake);
    assume property (sig_a |-> !sig_b);            // formal input constraint
endchecker
 
// ── Instantiate: in a module / via bind ─────────────────────────────
my_chk u_chk (.clk(clk), .rst_n(rst_n), .sig_a(a), .sig_b(b));
my_chk u_chk (.*);                                  // implicit connection
bind target_mod  my_chk u_chk (.clk(clk), .rst_n(rst_n), .sig_a(a), .sig_b(b));
 
// Rules: input/output ports only · automatic vars · verification-only (no synthesis)

14. Summary

A checker is SystemVerilog's purpose-built home for assertions: a module-shaped, verification-only container with automatic per-instance variables, body-wide default clocking and default disable iff, scoped sequence/property names, and free variables for formal proof. Those features fix the real problems of loose assertions — repeated clock/reset boilerplate, namespace clashes, shared static state across instances, and the missing formal story.

You instantiate a checker like a module — directly in a design block, inside an interface so every user inherits it, or non-invasively via bind onto RTL you don't own (the production pattern, composing with the previous lesson). The AHB-Lite example shows the payoff: three protocol rules and a coverage deck in one reusable unit, where the coverage report doubles as a to-do list for the testbench. Choose checker over module for any new assertion deck — the automatic variables and one-place clock/reset defaults make it safer and cleaner — and reserve module for the rare cases needing inout ports or synthesizable behaviour. A checker never reaches synthesis: assertions, coverage, and trackers only.