Lesson 2.2 turned DCRouter's sleep sentence into numbered rules: asleep means nothing accepted or sent; any valid input wakes it next cycle; it never sleeps mid-packet. Those rules were written to be checked. Until now nothing in the testbench checked them directly; the scoreboard only noticed when their violation eventually corrupted or stalled traffic.

How do you check a rule every cycle, at the place it applies?

The obvious answer, and why it breaks

The obvious approach writes procedural checks in the testbench: an always block that tests the condition and prints an error. That works for simple cases and becomes unreadable for anything about time: "within three cycles", "in the next cycle", "until". Each temporal rule turns into a small hand-built state machine, and each state machine is a new place for a testbench bug. SystemVerilog Assertions state such rules directly (fact V1).

The idea: one rule, one assertion

Good assertions are named after their rule, use only pins and documented state, and say in their failure message which rule broke.

Build it: DCRouter step 6

Seven assertions on DCRouter's pins. A small monitor mirrors CTRL by watching APB writes, so the assertions know which ports are enabled and whether low power is on; idle_run counts cycles with nothing in flight, from the environment's own bookkeeping.

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
26
27
28
29

// dcr_sva.svh: DCRouter step 6, local checkers. Concurrent assertions on DCRouter's pins, included
// inside `module tb` after dcr_env.svh. Each assertion is one rule; a failure names it.
// ctrl_q mirrors CTRL by watching APB writes, so checks know the current configuration.
logic [5:0] ctrl_q = 6'h3F;
always @(posedge clk) if (psel && penable && pwrite && paddr == 8'h00) ctrl_q <= pwdata[5:0];
int idle_run = 0;                                  // cycles with nothing in flight anywhere
always @(posedge clk) idle_run <= (pending() == 0 && in_vld == 0 && in_pkt.sum() with (int'(item)) == 0) ? idle_run + 1 : 0;

// R1: a disabled port is never ready
a_r1_disabled: assert property (@(posedge clk) disable iff (rst) (in_rdy & ~ctrl_q[3:0]) == 4'b0)
  else fail("R1: in_rdy high on a disabled port");
// R5, R8: out_err appears only on a tail
a_r8_err_on_tail: assert property (@(posedge clk) disable iff (rst) (out_err & ~out_last) == 4'b0)
  else fail("R8: out_err without out_last");
// R12: pslverr only in the access phase
a_r12_access: assert property (@(posedge clk) disable iff (rst) pslverr |-> psel && penable)
  else fail("R12: pslverr outside an access phase");
// R13: asleep, nothing is accepted or sent
a_r13_quiet: assert property (@(posedge clk) disable iff (rst) sleeping |-> in_rdy == 4'b0 && out_vld == 4'b0)
  else fail("R13: traffic while sleeping");
// R13: any valid input wakes the router in the next cycle
a_r13_wake: assert property (@(posedge clk) disable iff (rst) sleeping && in_vld != 4'b0 |=> !sleeping)
  else fail($sformatf("R13: in_vld %b did not wake the router", $past(in_vld)));
// R13: never asleep while a packet is part-way out of an output
a_r13_no_lock: assert property (@(posedge clk) disable iff (rst) $rose(sleeping) |-> in_pkt.sum() with (int'(item)) == 0)
  else fail("R13: fell asleep in the middle of a packet");
// R13: with lp_en, asleep within 10 cycles of everything going idle
a_r13_sleep: assert property (@(posedge clk) disable iff (rst) ctrl_q[5] && idle_run > 10 |-> sleeping)
  else fail("R13: idle for 10 cycles but not sleeping");

The stimulus is lesson 4.10's random hunt, unchanged, packaged as tasks so later lessons can reuse it:

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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

// dcr_hunt.svh: the constrained-random hunt of lesson 4.10, packaged as tasks. Included inside
// `module tb` after dcr_env.svh. hunt() runs 12 random rounds; final_checks() compares the
// counters with what the testbench saw and audits the credits.
class packet;
  rand bit [1:0] dst;
  rand bit       prio;
  rand bit [3:0] len;
  rand bit       bad;
  constraint c_len { len dist {0 := 2, 1 := 10, [2:14] :/ 70, 15 := 18}; }   // percent
  constraint c_bad { len != 0 -> bad dist {0 := 95, 1 := 5};
                     len == 0 -> !bad; }                                    // one fault per packet
endclass
int hunt_gaps [3] = '{0, 40, 92};
int hunt_drains [3] = '{100, 40, 4};

task automatic hunt();
  packet p = new();
  bit [3:0] active;
  for (int r = 0; r < 12; r++) begin
    active = 4'($urandom_range(1, 15));
    apb_wr(8'h00, {26'b0, 1'b1, 1'($urandom_range(0, 1)), 4'hF});   // lp_en, random prio_en, all ports on
    for (int k = 0; k < 4; k++) begin
      gap_pct[k] = hunt_gaps[$urandom_range(0, 2)];
      drain_pct[k] = hunt_drains[$urandom_range(0, 2)];
    end
    for (int n = 0; n < 10; n++)
      for (int i = 0; i < 4; i++)
        if (active[i]) begin
          if (!p.randomize()) fail("randomize failed");
          queue_pkt(i, p.dst, p.prio, p.len, p.bad);
        end
    wait_drain(40000);
    repeat ($urandom_range(0, 30)) @(posedge clk);
  end
endtask

task automatic final_checks();
  int n0;
  for (int k = 0; k < 4; k++) check_reg(8'h20 + 8'(4 * k), got_pkts[k], $sformatf("PKT_CNT%0d", k));
  for (int k = 0; k < 4; k++) check_reg(8'h10 + 8'(4 * k), bad_pkts[k] > 255 ? 255 : bad_pkts[k], $sformatf("ERR_CNT%0d", k));
  gap_pct = '{0, 0, 0, 0};
  drain_pct = '{100, 100, 100, 100};
  while (occ.sum() > 0) @(posedge clk);
  repeat (2) @(posedge clk);
  for (int o = 0; o < 4; o++) begin
    drain_pct[o] = 0;
    n0 = got_flits[o];
    queue_pkt(0, o, 0, 15);
    repeat (60) @(posedge clk);
    if (got_flits[o] - n0 != 4) fail($sformatf("credit audit: %0d flits left output %0d into a stalled sink, expected 4", got_flits[o] - n0, o));
    drain_pct[o] = 100;
    wait_drain();
  end
endtask

The testbench is now three includes and three calls:

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

// uses: dcrouter
// DCRouter step 6: lesson 4.10's random hunt with the local checkers of dcr_sva.svh added.
module tb;
  `include "dcr_env.svh"
  `include "dcr_hunt.svh"
  `include "dcr_sva.svh"
  initial begin
    reset_dut();
    hunt();
    final_checks();
    finish($sformatf("random hunt with assertions: %0d packets, no assertion failed", sent_pkts.sum()));
  end
endmodule

It passes on the clean design. Against the Bug Zoo:

clean design: PASS
  BUG_1  caught  ERROR @855: out0: unexpected flit 3d43
  BUG_2  caught  ERROR @135: out1: flit 0000, expected 3b10 from input 3
  BUG_3  caught  ERROR @4165: out1: out_err 1 on flit 2811, expected 0
  BUG_4  caught  ERROR @189155: out2: out_err 0 on flit 00e2, expected 1
  BUG_5  missed  
  BUG_6  missed  
  BUG_7  missed  
  BUG_8  caught  ERROR @85: out1: out_err 1 on flit 7580, expected 0
  BUG_9  caught  ERROR @310245: credit audit: 1 flits left output 0 into a stalled sink, expected 4
  BUG_10 caught  ERROR @216575: credit audit: 3 flits left output 0 into a stalled sink, expected 4
  BUG_11 caught  ERROR @240345: PKT_CNT3: read 4a, expected 4c
  BUG_12 caught  ERROR @4975: out3: out_err 1 on flit 0037, expected 0
  BUG_13 caught  ERROR @36725: out2: out_err 0 on flit 0084, expected 1
  BUG_14 caught  ERROR @240435: ERR_CNT2: read 32, expected 4
  BUG_15 missed  
  BUG_16 missed  
  BUG_17 missed  
  BUG_18 missed  
  BUG_19 missed  
  BUG_20 caught  ERROR @36815: R13: fell asleep in the middle of a packet
  BUG_21 caught  ERROR @39985: R13: in_vld 1000 did not wake the router
  BUG_22 caught  ERROR @255105: credit audit: 2 flits left output 0 into a stalled sink, expected 4
  BUG_23 missed  
  BUG_24 caught  ERROR @785: out0: unexpected flit ff82
caught 15 of 24 bugs

What the assertions changed

How to read it: the count is unchanged at 15 of 24, because the scoreboard already caught both bugs. What changed is when and how. BUG_21 is now reported at 39985 ns instead of 439965 ns, about eleven times earlier, and the message names the rule and shows that only input 3 was valid. BUG_20 is reported at the moment the router fell asleep, as a rule violation instead of a corrupted flit. None of the assertions fired on the clean design, and the R1 assertion never got a chance to fire at all, because the random hunt never disables a port; that gap waits for Part 6.

Writing assertions that help

• One rule per assertion, named after it: a failure should say which sentence of the specification broke.

• Pins and documented state only: internal-signal assertions belong to designers (lesson 3.4).

• Disable during reset, and think about the first cycles after it.

• Know whether each assertion was exercised: an assertion that guards a condition the stimulus never creates passes without ever being tested, as R1 did here: no test disabled a port. For implications this is called vacuity (lesson 5.8).

How real teams use assertions

What breaks

This step caught no new bugs, and that is a lesson too. Assertions are not a separate source of bugs; they are faster, more precise detection of rule violations the stimulus causes. Three of the five bugs no test has caught yet (BUG_5, 6, 7) break arbitration rules, which no simple pin assertion can express (the other two, BUG_16 and BUG_23, are never even reached; that is Part 6's problem); lesson 5.10 needs a checker with a model of who was waiting.

Key takeaways

• An assertion checks one rule every cycle where it applies, and fails at the cause.

• On DCRouter, assertions found no new bugs but reported BUG_21 eleven times earlier, naming the rule.

• An assertion whose condition never occurs proves nothing: check that it was exercised.

Related topics

• Part 5 overview: Checking

• SystemVerilog course: Assertions