One reusable checker

A real protocol check needs auxiliary modeling, several assertions, and shared clock and reset plumbing. checker packages all of that into one verification-only unit that instantiates anywhere a concurrent assertion is legal.

The checker below is not run in this course's checks: Verilator 5.048 stops with an internal error on it, and Icarus 13 has no checker construct.

1
2
3
4
5
6
7
8
9
10
11
12

// not-run: Verilator 5.048 stops with an internal error on this checker; Icarus 13 has no checker construct
checker req_ack_chk (
  logic req, ack, clk, rst_n
);
  default clocking @(posedge clk); endclocking
  default disable iff (!rst_n);

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

Defaults remove per-property clock and reset boilerplate. All ports stay explicit, so every instantiation names its clock and reset.

// snippet
bind link req_ack_chk u_link_chk (.req(req), .ack(ack), .clk(clk), .rst_n(rst_n));

Bind from a separate file needs zero RTL edits, and the connection can name internal signals. Prefer plain modules with bind for checks that must run in every simulator; reach for checker when the library targets formal tools or needs free variables.

One watched address instead of a memory

A free variable is a rand variable that no one assigns. Declared rand const, it is chosen once, nondeterministically, and then held: in formal the prover covers every value, and a simulator picks one value per run. Plain rand takes a new value every cycle, so it cannot stand for one watched address.

The checker below is not run in this course's checks: Verilator 5.048 supports neither checker parameters nor checker rand variables, and Icarus 13 has no checker construct.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

// not-run: Verilator 5.048 supports neither checker parameters nor checker rand variables; Icarus 13 has no checker construct
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, held: one symbolic address

  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

Silence by policy, not by edit

disable iff handles reset per property, but it cannot cover phases the author never anticipated. Control tasks act from the outside: testbench code switches whole scopes off and on at runtime.

$assertoff stops new attempts but lets in-flight attempts finish. $assertkill also terminates the in-flight threads, so kill is the right call around reset.

The reset policy below is not run in this course's checks because it is a fragment: it names a tb_top.dut hierarchy that is not defined here.

1
2
3
4
5
6
7

// not-run: fragment; tb_top.dut and tb_top.rst_n are not defined here
initial begin
  $assertkill(0, tb_top.dut);
  wait (tb_top.rst_n === 1'b1);
  repeat (2) @(posedge tb_top.clk);
  $asserton(0, tb_top.dut);
end

The testbench below runs the declarative half of the same policy here. Reset-phase stimulus would fail if it were ever enabled, and clean traffic passes after. Then a planted dropped request runs twice: under $assertoff, where it must stay silent, and after $asserton, where it must be reported.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

module link_sm (
  input  logic clk,
  input  logic rst_n,
  input  logic bug,          // planted: requests are dropped
  input  logic req,
  output logic ack
);
  logic [1:0] dly;
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin dly <= '0; ack <= 1'b0; end
    else begin dly <= {dly[0], req && !bug}; ack <= dly[1]; end
endmodule

module link_sm_checks (
  input logic clk, rst_n, req, ack
);
  int n_fail = 0;
  function automatic void fail(string msg);
    n_fail++;
    $display("[%0t] %m: %s", $time, msg);
  endfunction
  ap_req_ack: assert property (@(posedge clk) disable iff (!rst_n)
    req |-> ##[1:4] ack)
    else fail("request was not acknowledged");
endmodule

reset noise and 2 requests: 2 acks, 0 reports
dropped request with $assertoff: 0 reports
[345000] tb_link_sm.mon.fail: request was not acknowledged
dropped request after $asserton: 1 report
PASS: reset noise stayed silent, $assertoff masked the planted drop, and $asserton caught it

Control codes, coverage and the global clock

SystemVerilog generalizes the three tasks into $assertcontrol, which adds control over pass and fail action blocks and over which assertion types are affected. The exact numeric control codes are LRM table material and are not quoted here.

Tools record attempts, real passes, vacuous passes and failures per assertion, plus hit counts per cover. That record is the audit trail proving the checks ran.

1
2
3
4

// snippet
// Save assertion coverage at the end of the run. $coverage_save takes the
// coverage type and a name; it saves data, it does not query counts.
final void'($coverage_save(`SV_COV_ASSERTION, "run1"));

Most teams read this data from tool reports and merged databases rather than the query tasks. A cover on the antecedent exposes checks that never really exercised.

// snippet
global clocking @(posedge clk); endclocking
// A property can then write @($global_clock) for the formal time base.

Global clocking nominates one clock as the formal reference clock. Simulation work only needs to recognize the syntax.

Related topics

• Protocol assertions

• Assertion debug

• Implication and vacuity