s1 and s2 matches when both operands match from the same start tick. The lengths may differ, and the composite ends with the longer operand.
s1 or s2 matches when either operand matches. It keeps every match from each side, so each or multiplies the live threads.
The second listing below is not run in this course's checks. Verilator 5.048 rejects its named sequences, because each has ## after its first item; the or itself works, and the bench writes the same rule inline.
// snippet
sequence s_addr_hs; avalid ##1 aready; endsequence // 2 ticks
sequence s_credit; crd_dec ##1 crd_dec ##1 crd_ok; endsequence // 3 ticks
property p_both;
// edge-anchored in real checkers; see antecedent-design
@(posedge clk) $rose(start) |-> (s_addr_hs and s_credit);
endproperty
// Composite ends when s_credit, the longer match, ends.// not-run: Verilator 5.048 rejects a named sequence with ## after its first item
sequence s_okay; resp_vld ##0 resp_okay; endsequence
sequence s_err; resp_vld ##0 resp_err ##1 err_logged; endsequence
property p_txn_done;
@(posedge clk) txn_launch |-> ##[1:8] (s_okay or s_err);
endpropertyComposer | Start rule | End rule |
|---|---|---|
| Both start together | Ends with the longer operand |
| Either starts | Each operand match is a match |
| Both start together | Operands must end together |
and. When does the composite match?At tick 12, the end of the longer operand. The shorter match ending at tick 11 does not end the composite.
s1 intersect s2 is and plus a length rule. Both operands must start together and end together, which rejects the drifted-endpoint pairings that and accepts.
The first pattern ends at slot 2 and the second at slot 3. The longer-end join completes at slot 3, and the equal-length join has no pairing.
Slot 0: idle, all pattern bits 0.
Slot 1: a and c rise, and both patterns start.
Slot 2: b rises, so the first pattern ends here.
Slot 3: d rises, so the second pattern ends here, and the longer-end join completes.
Slot 4: both low again, and no equal-length pairing ever existed.
The idiom 1 [*M:N] intersect s turns this rule into a tool. It constrains a variable-length sequence to take between M and N cycles.
The length-bounding listing below is not run in this course's checks. Verilator 5.048 stopped with an internal error on intersect, with or without a default clocking block.
// not-run: Verilator 5.048 stops with an internal error on intersect
sequence s_handshake; req ##[1:$] ack ##1 done; endsequence
property p_hs_4to8;
@(posedge clk) start |-> (1 [*4:8] intersect s_handshake);
endpropertyintersect. What does the check do?It never matches. A structurally unsatisfiable intersect fails every time, so verify the length sets overlap before writing it.
expr throughout seq holds a boolean over every tick of a sequence match, from its first cycle to its last. The left side must be a boolean expression, never a sequence.
s1 within s2 places a whole pattern inside a window. The inner match may start and end anywhere inside the outer span, including on its edges.
Both listings below are not run in this course's checks because Verilator 5.048 does not support an unbounded repetition ([*1:$]) inside throughout or within.
// not-run: Verilator 5.048 does not support [*1:$] inside throughout
// No abort for the whole burst: start through last beat
property p_no_abort_in_burst;
@(posedge clk) burst_start |-> (!abort) throughout (burst_start ##1 beat [->4]);
endproperty
// Stable config during a transaction
property p_cfg_stable;
@(posedge clk) txn_start |->
$stable(cfg_mode) throughout (txn_active [*1:$] ##1 txn_done);
endproperty// not-run: Verilator 5.048 does not support [*1:$] inside within
// The req/ack handshake must complete inside the frame window
sequence s_frame;
frame_start ##1 frame_act [*1:$] ##1 frame_end;
endsequence
property p_hs_in_frame;
@(posedge clk) frame_start |-> ((req ##[1:4] ack) within s_frame);
endpropertyNeed | Operator | Operand shape |
|---|---|---|
A condition true at every tick of a window |
| Boolean over a sequence |
A pattern occurring somewhere inside a window |
| Sequence inside a sequence |
A sequence bounded to M..N cycles |
| Sequence against a timer |
throughout. What is wrong?The left operand must be a boolean expression. A pattern placed in a window needs within instead.
within. Does the composite match?No. Containment is violated, so the handshake leaked past the frame and there is no match.
The bench runs the three composers for real. Each composite gets a cover, which counts its matches, and an assertion form that Verilator checks correctly: p |-> (s1 and s2) checks exactly what two implications p |-> s1 and p |-> s2 check, and the or rule splits into a one-step check per branch plus a timeout whose range sits at the end.
and assert report? How many did Verilator report?Four, one per broken pair. Verilator reported 2: it caught the late breaks and missed the early ones. The two split implications caught all 4.
module tb_join;
logic clk = 0, start = 0;
logic avalid = 0, aready = 0, crd_dec = 0, crd_ok = 0;
logic txn_launch = 0, resp_vld = 0, resp_okay = 0, resp_err = 0, err_logged = 0;
logic burst_start = 0, abort = 0;
always #5 clk = ~clk;
int and_fails = 0, and_hits = 0, split_fails = 0, resp_fails = 0, log_fails = 0, timeouts = 0, or_hits = 0, thr_fails = 0;
// and: both patterns from the same start. Written inline; the cover counts matches.
ap_both: assert property (@(posedge clk) $rose(start) |-> ((avalid ##1 aready) and (crd_dec ##1 crd_dec ##1 crd_ok))) else and_fails++;
cp_both: cover property (@(posedge clk) $rose(start) ##0 ((avalid ##1 aready) and (crd_dec ##1 crd_dec ##1 crd_ok))) and_hits++;
// The same obligation as two implications: "p |-> (s1 and s2)" checks exactly what these two check.
ap_addr: assert property (@(posedge clk) $rose(start) |-> avalid ##1 aready) else split_fails++;
ap_credit: assert property (@(posedge clk) $rose(start) |-> crd_dec ##1 crd_dec ##1 crd_ok) else split_fails++;
// or: a response is okay, or an error that gets logged the tick after.
cp_done: cover property (@(posedge clk) resp_vld ##0 ((resp_okay) or (resp_err ##1 err_logged))) or_hits++;
// The same rule split into one-step checks, plus the timeout with its range at the end.
ap_resp: assert property (@(posedge clk) resp_vld |-> resp_okay || resp_err) else resp_fails++;
ap_logged: assert property (@(posedge clk) resp_vld && resp_err |=> err_logged) else log_fails++;
ap_timeout: assert property (@(posedge clk) $rose(txn_launch) |-> ##[1:8] resp_vld) else timeouts++;
// throughout over a fixed window: no abort for the 4 ticks starting at burst_start.
ap_noabort: assert property (@(posedge clk) $rose(burst_start) |-> (!abort) throughout (1'b1 [*4])) else thr_fails++;
task automatic pair(int kind); // 0 good; 1 crd_ok never comes; 2 crd_dec drops on tick 2
@(negedge clk) start = 1; avalid = 1; crd_dec = 1;
@(negedge clk) start = 0; avalid = 0; aready = 1; crd_dec = (kind != 2);
@(negedge clk) aready = 0; crd_dec = 0; crd_ok = (kind != 1);
@(negedge clk) crd_ok = 0;
repeat (3) @(negedge clk);
endtask
task automatic txn(int kind); // 0 okay, 1 error logged, 2 error not logged
@(negedge clk) txn_launch = 1;
@(negedge clk) txn_launch = 0;
repeat (2) @(negedge clk);
resp_vld = 1; resp_okay = (kind == 0); resp_err = (kind != 0);
@(negedge clk) resp_vld = 0; resp_okay = 0; resp_err = 0; err_logged = (kind == 1);
@(negedge clk) err_logged = 0;
repeat (8) @(negedge clk);
endtask
task automatic burst(int abort_at);
@(negedge clk) burst_start = 1;
for (int i = 0; i < 6; i++) begin abort = (i == abort_at); @(negedge clk); burst_start = 0; end
abort = 0;
repeat (3) @(negedge clk);
endtask
initial begin
repeat (2) @(negedge clk);
for (int i = 0; i < 6; i++) pair(0);
for (int i = 0; i < 2; i++) pair(1); // planted: breaks on the last tick
for (int i = 0; i < 2; i++) pair(2); // planted: breaks on the second tick
$display("and over 10 pairs (2 break late, 2 break early): cover %0d matches; inline and assert %0d failures; split asserts %0d failures",
and_hits, and_fails, split_fails);
for (int i = 0; i < 4; i++) txn(0);
for (int i = 0; i < 4; i++) txn(1);
for (int i = 0; i < 2; i++) txn(2); // planted: an error that is never logged
$display("or over 10 responses (2 unlogged errors): cover %0d matches; split checks %0d + %0d failures; %0d timeouts",
or_hits, resp_fails, log_fails, timeouts);
burst(-1); burst(-1); burst(2); burst(5); // abort inside the window at 2; after it at 5
$display("throughout: %0d failure for an abort inside the 4-tick window, none for one after it", thr_fails);
if (and_hits != 6 || split_fails != 4 || or_hits != 8 || log_fails != 2 || resp_fails != 0 || timeouts != 0 || thr_fails != 1)
$fatal(1, "FAIL: %0d %0d %0d %0d %0d %0d %0d", and_hits, split_fails, or_hits, log_fails, resp_fails, timeouts, thr_fails);
$display("PASS: the covers counted the right matches, the split checks caught every planted bug, and throughout caught the abort");
$finish;
end
endmoduleand over 10 pairs (2 break late, 2 break early): cover 6 matches; inline and assert 2 failures; split asserts 4 failures
or over 10 responses (2 unlogged errors): cover 8 matches; split checks 0 + 2 failures; 0 timeouts
throughout: 1 failure for an abort inside the 4-tick window, none for one after it
PASS: the covers counted the right matches, the split checks caught every planted bug, and throughout caught the abortRun 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.
The inline and assert caught 2 of 4 broken pairs (the late breaks); the two split implications caught 4. Covers counted 6 and 8 matches, both right. intersect stopped Verilator with an internal error.