Part 4 · Assertions (SVA) · Intermediate
and, or, intersect
Sequence conjunction with different lengths, or-branch threads, and intersect's same-length constraint.
Sequence and: both match, lengths may differ
s1 and s2 matches when both operands match threads that start at the same tick. The lengths may differ: the composite match ends when the longer of the two matching threads ends. This is sequence-level and — both temporal patterns occur, anchored to a common start — and is entirely different from boolean &&, which compares two expressions within one tick.
// Both the addr handshake AND the credit check must occur,
// starting together; they may finish at different times.
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;
@(posedge clk) start |-> (s_addr_hs and s_credit);
endproperty
a_both: assert property (p_both);
// Composite ends when s_credit (the longer match) ends.WAVEFORM — s_addr_hs and s_credit (attempt at tick 2)
clk : 1 2 3 4 5
avalid : 0 1 0 0 0
aready : 0 0 1 0 0
crd_dec : 0 1 1 0 0
crd_ok : 0 0 0 1 0
A
s_addr_hs : starts @2, matches @3 ──┐ (shorter)
s_credit : starts @2, matches @4 ──┴─► AND matches @4
m1 M
M = composite endpoint = end of the LONGER operand (tick 4).
If either operand never matches from tick 2 → no composite match.Sequence or: branching threads
s1 or s2 matches when either operand matches from the shared start tick — it simply forks both operand thread sets and keeps every match from each. Each operand match is a separate composite match, so or multiplies match threads : (3 threads) or (2 threads) evaluates up to 5. Useful for protocol alternatives — a transaction completes by OKAY or by ERROR — but each or is also a thread-count multiplier to keep in mind for simulator performance.
// Transaction terminates with okay-response or error-response path
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);
endproperty
a_done: assert property (p_txn_done);WAVEFORM — s_okay or s_err (operands start at tick 3)
clk : 1 2 3 4 5
resp_vld : 0 0 1 0 0
resp_okay : 0 0 0 0 0
resp_err : 0 0 1 0 0
err_logged : 0 0 0 1 0
A
s_okay branch: resp_okay=0 @3 → branch dies
s_err branch: resp_err=1 @3, err_logged=1 @4 → MATCH @4
M
or = union of the two branches' matches; one survivor suffices.intersect: both match with the SAME length
s1 intersect s2 is and plus a length equality constraint : both operands must match starting at the same tick AND ending at the same tick. This is the tool for pinning a pattern to an exact-duration window — "the handshake completes in exactly the cycles the frame is active" — and for eliminating false matches that and would allow by letting operand endpoints drift apart. A classic idiom: 1[*M:N] intersect s constrains a variable-length sequence s to take between M and N cycles.
// The retry sequence must take EXACTLY the frame's duration
property p_retry_fits_frame;
@(posedge clk) frame_start |->
( (frame_act [*1:$] ##1 frame_end)
intersect
(retry ##1 retry_busy [*1:$] ##1 retry_done) );
endproperty
// Idiom: bound an unbounded sequence's length to 4..8 cycles
sequence s_handshake; req ##[1:$] ack ##1 done; endsequence
property p_hs_4to8;
@(posedge clk) start |-> (1 [*4:8] intersect s_handshake);
endproperty
a_hs: assert property (p_hs_4to8);WAVEFORM — and vs intersect on the same stimulus
s1 = a ##1 b s2 = c ##[1:2] d
clk : 1 2 3 4
a : 0 1 0 0
b : 0 0 1 0
c : 0 1 0 0
d : 0 0 0 1
A
s1: starts @2, matches @3 (length 2)
s2: thread d@3 → d=0 dies; thread d@4 → MATCH @4 (length 3)
s1 and s2 : both matched from @2 → MATCH, ends @4
s1 intersect s2 : lengths 2 vs 3 → NO equal-length pairing → FAIL
intersect rejects the drifted-endpoint pairing that and accepted.Choosing the right composer
Decision summary
and — both patterns occur from a common start; end times independent; composite ends with the longer.
or — at least one pattern occurs; union of matches; multiplies threads.
intersect — both occur with identical start AND end; the duration-pinning tool.
1[*M:N] intersect s — the standard idiom to length-bound a sequence (also see within, next lesson).
Interview angle
"Difference between and and intersect?" — the one-line answer is length: and allows different end ticks, intersect requires identical ones. Then draw the drifted-endpoint waveform above.
"Is sequence and the same as &&?" — no: && is one-tick boolean conjunction; and composes multi-cycle patterns from a shared start.
"How do you force a sequence to take exactly N cycles?" — 1[*N] intersect s (or s within a fixed window for containment instead of equality).
"Why might or hurt simulation performance?" — every or doubles the live thread sets per attempt; nested ranged-or stacks multiply quickly.
Key takeaways
All three composers anchor operands to a common start tick; they differ in end-tick rules.
and ends with the longer operand; intersect demands equal length; or keeps every operand match.
intersect is the precision tool — use it when endpoint drift would create false matches.
1[*M:N] intersect s is the canonical length-bounding idiom for variable-length sequences.
Common pitfalls
Using and when the spec requires simultaneous completion — endpoint drift silently passes wrong behavior; you wanted intersect.
Confusing sequence and with boolean && inside an expression — different operators, different layers.
intersect between sequences whose possible lengths never coincide — a structurally unsatisfiable check that fails (or vacuously never matches) every time.
Stacking or of wide ##[M:N] ranges — match-thread explosion; bound ranges or restructure.
Forgetting both operands of and/intersect must START together — neither operator lets one sequence begin mid-way through the other (that is within).