Holding until an event: until and throughout

Two questions for every hold

Every "p holds until q" rule has to answer two questions. Must p still hold at the edge where q arrives? And must q arrive before the test ends? Get either answer wrong, and the rule passes a real bug or fails on legal traffic. The four until operators are the four combinations of answers.

In each form, p must hold at every edge from the start of the attempt until q is seen. The difference is only the last edge, and what happens if that edge never comes.

One trace, two operators

The two figures below follow three attempts on one trace. In A, v drops exactly where r arrives. In B, r is already high at the start. In C, r never comes before the test stops.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic start = 0, v = 0, r = 0;

  hold_until: assert property (@(posedge clk) start |-> v until r);

  initial begin
    @(negedge clk); start = 1; v = 1;   // A starts at 15
    @(negedge clk); start = 0;
    @(negedge clk); v = 0; r = 1;       // r at 35, v already low
    @(negedge clk); r = 0;
    @(negedge clk); start = 1; r = 1;   // B starts at 55 with r already high
    @(negedge clk); start = 0; r = 0;
    @(negedge clk); start = 1; v = 1;   // C starts at 75; r never comes
    @(negedge clk); start = 0;
    @(negedge clk);
    @(negedge clk);
    $finish;                            // the test stops at 100
  end
endmodule

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic start = 0, v = 0, r = 0;

  hold_until_with: assert property (@(posedge clk) start |-> v until_with r);

  initial begin
    @(negedge clk); start = 1; v = 1;   // A starts at 15
    @(negedge clk); start = 0;
    @(negedge clk); v = 0; r = 1;       // r at 35, v already low
    @(negedge clk); r = 0;
    @(negedge clk); start = 1; r = 1;   // B starts at 55 with r already high
    @(negedge clk); start = 0; r = 0;
    @(negedge clk); start = 1; v = 1;   // C starts at 75; r never comes
    @(negedge clk); start = 0;
    @(negedge clk);
    @(negedge clk);
    $finish;                            // the test stops at 100
  end
endmodule

Lane A is the whole difference between the two. For a hold that must cover the transfer itself, such as data that must be right when rready is seen, only the overlapping form works: rvalid && !rready |=> (rvalid && $stable(rdata)) until_with rready.

The hold rule, edge by edge

1. Edge 1: the offer stalls

   The antecedent rvalid && !rready matches, so an attempt starts. Because of |=>, the hold begins at the next edge.

2. Edge 2: still stalled

   rvalid is high and rdata equals its value at edge 1, so $stable holds. rready is still low, so the attempt keeps going.

3. Edge 3: the transfer

   rready is seen, so this is the last edge the attempt checks. Because the operator is until_with, rvalid and stable data must hold here as well.

Each stalled edge also starts its own attempt, so a three-edge stall is checked by overlapping attempts that all end at the transfer. A data change anywhere in the stall fails at least one of them.

When the event is already there

Lane B is the trap from the opening story. If q is true at the first edge of the attempt, until passes without checking anything, and until_with checks p on that single edge only. A leftover gnt, a sticky done or a level that stays high between transfers all end the hold before it starts.

Decide whether the first edge counts. If the event must be a new one, skip that edge: req throughout (##1 gnt[->1]) waits for the first gnt after the start edge. Writing the event as an edge, req until $rose(gnt), has the same effect when gnt is a level that stays high.

throughout

c throughout s requires the boolean c at every edge of a match of the sequence s, from its first edge to its last. s can be fixed, en throughout (##2 done), or a window, en throughout (##[1:3] d). Unlike the operands of until, which are properties, the left side here must be a plain boolean expression.

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                 // rising edges at 5, 15, 25, ...
  logic s = 0, en = 0, d = 0;

  en_until_d: assert property (@(posedge clk) s |-> en throughout (##[1:3] d));

  initial begin
    @(negedge clk); s = 1; en = 1;      // start at 15
    @(negedge clk); s = 0;
    @(negedge clk); d = 1;              // d at 35, en still high
    @(negedge clk); d = 0; en = 0;
    @(negedge clk); s = 1; en = 1;      // start at 55
    @(negedge clk); s = 0;
    @(negedge clk); en = 0;             // en drops at 75
    @(negedge clk); d = 1;              // d at 85: too late
    @(negedge clk); d = 0;
    @(negedge clk);
    $finish;
  end
endmodule

A window under throughout is a bounded hold: "en stays high, and d comes within three edges". It fails at a definite edge, which makes it the simulation-friendly cousin of s_until.

Over a goto, v throughout r[->1] gives the same verdicts as v until_with r. The example measures all five operators on one trace.

Because throughout builds a sequence, the standard also lets more sequence follow it. That use is not covered yet.

Choosing the operator

Keep "what must hold while waiting" and "how long the wait may last" as two rules. A weak hold rule plus a bounded latency rule, such as rvalid && !rready |-> ##[0:16] rready, gives two failure messages, and each names the requirement that broke. One strong rule that mixes both reports only at the end of the run, and says less.

Try it

Attempts A and B are the lanes of the figures. The non-overlapping forms pass both; the overlapping forms, and throughout over a goto, fail both. Attempt C here gets its r at 95 with v still high, so every operator passes it.

Delete the line that raises r at 95. The weak forms then stay silent, and Verilator stops at $finish with an error for the two strong ones.

Check yourself

module tb;
  logic clk = 0;
  always #5 clk = ~clk;                  // rising edges at 5, 15, 25, ...
  logic v = 0, r = 0;
  p: assert property (@(posedge clk) v && !r |=> v until_with r)
    else $display("fail at %0t", $time);
  initial begin
    @(negedge clk); v = 1;               // stalled at 15
    @(negedge clk); r = 1;               // transfer at 25
    @(negedge clk); v = 0; r = 0;
    @(negedge clk); v = 1;               // stalled at 45
    @(negedge clk); v = 0; r = 1;        // valid gone at the ready edge, 55
    @(negedge clk); r = 0;
    #20 $finish;
  end
endmodule

rvalid && !rready |=> (rvalid && rdata == $past(rdata)) until_with rready

rvalid && !rready |=> (rvalid && $stable(rdata)) until_with rready

rvalid && !rready |=> (rvalid && $stable(rdata)) until rready

rvalid && !rready |-> ##1 ((rvalid && $stable(rdata)) until_with rready)

$rose(req) |-> req throughout (##1 gnt[->1])

$rose(req) |=> req until_with gnt

$rose(req) |-> req until $rose(gnt)

$rose(req) |-> req until gnt

Practice

• Hold the offer Verify · Easy