a ##2 b means a holds on one sampled tick and b holds exactly two ticks later. Ticks are edges of the sequence clock, never nanoseconds.
// snippet
sequence s_req_gnt;
req ##2 gnt; // matches iff req at tick T and gnt at tick T+2
endsequence
property p_fixed_gnt;
// edge-anchored in real checkers; see antecedent-design
@(posedge clk) $rose(req) |-> ##2 gnt;
endpropertyForm | Meaning | Threads |
|---|---|---|
|
| One |
|
| One |
|
| One per delay |
|
| Unbounded, weak |
|
| One, fused |
gnt arrives one tick after req under req ##2 gnt. Does the sequence match?No. A fixed delay means exactly N ticks, so an early arrival misses exactly like a late one.
a ##[1:3] b accepts b one, two, or three ticks after a. The attempt forks three threads at once, and whichever thread sees b is a match.
Several threads can match from one attempt. That is normal, and later lessons prune the extras with first_match.
The request at slot 1 is answered at slot 4. The fixed delay misses, and the ranged delay matches through its third thread.
Slot 0: idle, req 0 and rsp 0.
Slot 1: req rises, and three threads start.
Slot 2: one tick on, rsp still 0, so the ##1 thread dies.
Slot 3: two ticks on, rsp still 0, so the ##2 thread dies.
Slot 4: rsp rises three ticks after the request, so the ##3 thread matches.
Slot 5: both low again.
b arrives twice inside a ##[1:3] window. How many matches does the attempt have?Two. Saying it takes the first one is wrong unless the sequence is wrapped in first_match.
a ##[1:$] b waits any number of ticks for b. A weak attempt that is still pending at the end of evaluation simply never completes; it never fails.
The strong operator differs: s_eventually b fails at the end of evaluation when b never arrived. That failure applies in simulation after $finish with a pending attempt, as well as in formal.
The trio below is not run in this course's checks because Verilator 5.048 does not support s_eventually.
// not-run: Verilator 5.048 does not support s_eventually
property p_weak_ack;
@(posedge clk) req |-> ##[1:$] ack; // ack may never come: no failure
endproperty
property p_strong_ack;
@(posedge clk) req |-> s_eventually ack; // unfulfilled at end of evaluation: failure
endproperty
property p_bounded_ack;
@(posedge clk) req |-> ##[1:64] ack; // practical answer: a checkable timeout
endpropertyPrefer the bounded form when a timeout must be checkable in simulation. A never-arriving ack under ##[1:$] passes silently and hides a dead handshake.
##[1:$] thread still waiting and an s_eventually attempt still waiting. Which one fails?Only the strong one. The weak delay never fails from waiting; the strong operator fails at the end of evaluation.
s1 ##0 s2 starts s2 on the tick where s1 ends. Between booleans it is conjunction; between phases it stitches back-to-back transfers with no idle cycle.
Overlapped implication uses the same fusion. The consequent starts on the antecedent endpoint, which is why |-> feels like a zero-delay join.
// snippet
sequence s_addr_phase;
valid ##1 addr_done; // ends on the addr_done cycle
endsequence
sequence s_data_phase;
data_valid ##1 data_done;
endsequence
sequence s_back_to_back;
s_addr_phase ##0 s_data_phase; // data phase starts where addr phase ends
endsequence##1 instead of ##0. Where does the second phase start?One cycle after the first phase ends. The ##1 inserts an idle cycle that fusion would have skipped.
The bench runs both rules as real assertions over 100 request pulses: 40 answered two ticks later, 20 after one tick, 20 after three and 20 after four. Each window ends with its range, which Verilator checks correctly.
##2 report over the 100 pulses? And ##[1:3]?60 for ##2: every answer that is not exactly two ticks late. 20 for ##[1:3]: only the four-tick answers.
module tb_delay_window;
logic clk = 0, req = 0, gnt = 0;
always #5 clk = ~clk;
int exact_fails = 0, window_fails = 0, reqs = 0;
// The two rules from this lesson, as real assertions.
ap_exact: assert property (@(posedge clk) $rose(req) |-> ##2 gnt) else exact_fails++;
ap_window: assert property (@(posedge clk) $rose(req) |-> ##[1:3] gnt) else window_fails++;
// One request pulse, answered lat ticks after the tick where req was sampled high.
task automatic send(int lat);
@(negedge clk) req = 1;
reqs++;
@(negedge clk) req = 0;
repeat (lat - 1) @(negedge clk);
gnt = 1;
@(negedge clk) gnt = 0;
repeat (4) @(negedge clk);
endtask
initial begin
repeat (2) @(negedge clk);
for (int i = 0; i < 40; i++) send(2);
for (int i = 0; i < 20; i++) send(1);
for (int i = 0; i < 20; i++) send(3);
for (int i = 0; i < 20; i++) send(4);
repeat (4) @(negedge clk);
$display("%0d requests: ##2 failed %0d times, ##[1:3] failed %0d times", reqs, exact_fails, window_fails);
if (exact_fails != 60 || window_fails != 20) $fatal(1, "FAIL: exact %0d window %0d", exact_fails, window_fails);
$display("PASS: the fixed delay passed only the 40 two-tick answers; the window passed 80 and caught the 20 four-tick answers");
$finish;
end
endmodule100 requests: ##2 failed 60 times, ##[1:3] failed 20 times
PASS: the fixed delay passed only the 40 two-tick answers; the window passed 80 and caught the 20 four-tick answersRun with Verilator 5.048 (--binary --timing --assert, plus --coverage when a listing has a cover property) on 2026-10-18; every bench printed the PASS line shown. Verilator stops at the first $error or failing assertion without an action block, so the benches count failures in the action block. Icarus 13 has no concurrent assertions.