Repetition and counting events

Consecutive repetition

b[*n] means b holds at n consecutive edges, the same as b ##1 b ##1 ... written out. $rose(rvalid) |-> rvalid[*4] says that once rvalid rises, it stays high for at least four edges, which every four-beat burst needs.

Whole sequences can repeat too: (rvalid ##1 !rvalid)[*2] describes valid going high and low twice in a row. Use this sparingly, because repeated sequences quickly become hard to read in a waveform.

A range at the end checks only its lower bound

b[*m:n] allows from m to n repetitions. At the end of a consequent it behaves like a delay range: the attempt passes at its first match, the shortest one. req |=> busy[*2:4] therefore passes as soon as busy has been high for two edges, and it still passes when busy stays high for six.

So the upper bound 4 checks nothing here. If the spec says "busy for two to four edges", the "at most four" half needs a rule of its own.

The upper bound needs its own rule

A fixed repetition can be a trigger. busy[*4] |=> !busy matches wherever busy has been high for four edges in a row, and then requires it low at the next edge. Each edge starts a new attempt, so a long stretch of busy starts several overlapping ones.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic req = 0, busy = 0;

  at_most_4: assert property (@(posedge clk) busy[*4] |=> !busy);

  initial begin
    @(negedge clk); req = 1;            // request sampled at 15
    @(negedge clk); req = 0; busy = 1;  // busy sampled at 25, 35, ... 75
    repeat (6) @(negedge clk);
    busy = 0;
    @(negedge clk); req = 1;            // request sampled at 95
    @(negedge clk); req = 0; busy = 1;  // busy only at 105
    @(negedge clk); busy = 0;
    repeat (2) @(negedge clk);          // edges at 115 and 125
    $finish;
  end
endmodule

Counting edges or counting events

Ask what the spec counts. Repetition counts clock edges, so it suits levels: "valid stays high for four edges", "busy never lasts more than four". A delay counts edges too.

Protocol rules usually count events: transfers, beats, grants. Written as an edge count, such a rule is right only while nothing stalls, which is exactly the trap in the opening story.

The standard has event-counting forms, the goto repetition [->n] and the non-consecutive repetition [=n]. They are not covered yet: Verilator 5.052 misses goto failures and rejects [=n]. Count the events in a few lines of ordinary code instead.

Counting with auxiliary code

A counter that resets on each request and increments on each transfer turns "the fourth transfer carries rlast" into xfer && beat == 3 |-> rlast, with stalls anywhere.

Such auxiliary code is common in real assertion suites. Keep it small and obviously correct, update it with nonblocking assignments at the clock, and remember that assertions see its value from before the edge, like any other signal.

assert property (@(posedge clk)
  req |-> ##4 rlast);

// beat: transfers since the request
assert property (@(posedge clk)
  xfer && beat == 3 |-> rlast);
assert property (@(posedge clk)
  xfer && beat < 3 |-> !rlast);

The second rule matters as much as the first. Without !rlast on earlier beats, a design that raises rlast on every beat passes.

Try it

The fixed-delay check failed the correct stalled burst at 115. On the faulty burst, the stall happened to put rlast exactly four edges after the request, so the fixed delay passed it. The transfer-counting rules caught the early rlast at 185 and the missing one at 195.

four_edges passed every burst, as it should. Change it to rvalid[*5] and predict which bursts fail it.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic req = 0, busy = 0;
  p: assert property (@(posedge clk) req |=> busy[*2:4])
    else $display("fail at %0t", $time);
  initial begin
    @(negedge clk); req = 1;             // request at 15
    @(negedge clk); req = 0; busy = 1;   // busy at 25 ... 75
    repeat (6) @(negedge clk);
    busy = 0;
    @(negedge clk); req = 1;             // request at 95
    @(negedge clk); req = 0; busy = 1;   // busy at 105 only
    @(negedge clk); busy = 0;
    repeat (2) @(negedge clk);
    $finish;
  end
endmodule

$rose(rvalid) |-> rvalid[*4]

$rose(rvalid) |-> rvalid ##1 rvalid ##1 rvalid ##1 rvalid

$rose(rvalid) |-> rvalid[*2:4]

$rose(rvalid) |=> rvalid[*3]