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.

systemverilog
// 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.
diagram
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.

systemverilog
// 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);
diagram
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.

systemverilog
// 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);
diagram
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).