Delays and ranges: one attempt, many threads

Fixed delays

##n moves the check n edges forward. req |-> ##2 ack requires ack exactly two edges after the request. ##0 joins two parts of a sequence at the same edge, and a |=> b is shorthand for a |-> ##1 b.

A fixed delay is right when the spec fixes the latency, such as a pipeline with three stages. Most handshakes allow a window instead, and a fixed delay then rejects legal designs that answer early or late.

A range forks threads

##[m:n] allows any delay from m to n edges. Inside one attempt, the range starts one thread per delay, and each thread looks at its own edge. The attempt passes at the first thread that matches, and the remaining threads are dropped.

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

  ack_soon: assert property (@(posedge clk) req |-> ##[1:3] ack);

  initial begin
    @(negedge clk); req = 1;            // requests sampled at 15 and 25
    @(negedge clk);
    @(negedge clk); req = 0;
    @(negedge clk); req = 1;            // request sampled at 45
    @(negedge clk); req = 0; ack = 1;   // one ack, sampled at 55
    @(negedge clk); ack = 0;
    repeat (2) @(negedge clk);          // edges at 65 and 75
    $finish;
  end
endmodule

Where a failure is reported

An attempt fails only when its last thread fails, so a missing response is reported at the end of the window. With ##[1:16], that is 16 edges after the request, however early the bug happened.

Two habits make such reports easy to read. Make the window as tight as the spec allows, so the report lands close to its cause. Print the attempt's start in the fail message, or capture an ID as lesson A4.1 shows, so the report names the request it belongs to.

A window wider than the spec is a quiet weakness too. A design that answers in 12 cycles passes a 16-cycle window even when the spec says 8. A window narrower than the spec is the opposite mistake: it fails legal designs, and the usual reaction is to switch the rule off.

A range is an or of delays

A sequence or matches when either operand matches. req |-> (##1 v) or (##2 v) passes when v comes one or two edges after the request, which is exactly what req |-> ##[1:2] v says. A range is the compact way to write alternatives that differ only in delay.

Two obligations from one trigger: and

A read request may need two independent answers: ack at the next edge and a status word three edges later. The sequence and says both: (##1 ack) and (##3 stat). Both operands start at the same edge, both must match, and the composite ends where the later one ends. Whatever follows starts from there.

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

  both_then_done: assert property (@(posedge clk) req |-> ((##1 ack) and (##3 stat)) ##1 done);

  initial begin
    @(negedge clk); req = 1;                     // request at 15
    @(negedge clk); req = 0; ack = 1;            // ack at 25
    @(negedge clk); ack = 0;
    @(negedge clk); stat = 1;                    // stat at 45
    @(negedge clk); stat = 0; done = 1;          // done at 55: in time
    @(negedge clk); done = 0; req = 1;           // request at 65
    @(negedge clk); req = 0; ack = 1;            // ack at 75
    @(negedge clk); ack = 0; done = 1;           // done at 85: too early
    @(negedge clk); done = 0; stat = 1;          // stat at 95
    @(negedge clk); stat = 0;                    // no done at 105
    @(negedge clk); req = 1;                     // request at 115
    @(negedge clk); req = 0;                     // no ack at 125
    @(negedge clk);
    @(negedge clk); stat = 1;                    // stat at 145
    @(negedge clk); stat = 0;
    $finish;
  end
endmodule

&& and and are different tools. ack && stat is one condition at one edge. and joins two sequences that may end at different edges.

With fixed delays, the same rule can be written as one chain, ##1 ack ##2 stat ##1 done. The and form keeps the two answers independent: each delay can change without rewriting the other, and the code reads like the spec.

Open windows, and what comes later

##[1:$] has no upper end: each attempt keeps one live thread per edge until a match, so a long-silent signal costs memory and time in every attempt. In simulation it also never fails, because a sequence used as an asserted property is weak by default (IEEE 1800-2017 16.12.2). The weakness comes from that default, not from the operator; lesson A3.1 shows the strong forms.

Ranges followed by more sequence, ranges in an antecedent and first_match are not covered yet: Verilator 5.052 misses some of their failures. End a sequence with its range, and check what follows from the event itself, as ack |=> done does in the example.

Try it

The first request is answered in two edges, so all three rules pass. The second is answered in one edge: legal by the spec, but exact_two fails at 85. The third is answered after four edges, so ack_soon fails at 145, the end of its window, and exact_two fails earlier, at 135.

The late ack at 155 has no done after it, and done_next reports that at 165. Move the last ack one edge earlier and predict which lines remain.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic req = 0, ack = 0;
  p: assert property (@(posedge clk) req |-> ##[1:3] ack)
    else $display("fail at %0t", $time);
  initial begin
    @(negedge clk); req = 1;             // request at 15
    @(negedge clk); req = 0;             // ack never comes
    #60 $finish;
  end
endmodule

req |-> ##[1:3] (rvalid == 1'b1)

req |=> ##[0:2] rvalid

req |-> ##1 rvalid

req |-> ##[1:3] rvalid