📋 What is a Sequence?

A sequence is a temporal pattern over sampled boolean expressions, evaluated at clock ticks. The simplest sequence is a single boolean expression — it matches at one clock tick if that expression is true. More complex sequences describe behaviours that span multiple clock ticks.

• A linear sequence is a finite ordered list of boolean expressions checked at consecutive clock ticks. It matches if every expression is true at its respective tick.
• A complex sequence uses operators to combine linear sequences — specifying choices, gaps, repetitions, and parallel requirements.
• Each evaluation attempt of a sequence starts at a specific clock tick and searches for a match from that starting point forward.
• Sequences are building blocks for properties — which are then used in assert, assume, and cover statements.

## Concatenation with ##

The ##N operator concatenates two sequence expressions with a cycle-count delay between them. ##1 means “one clock tick after”, ##0 means “at the same clock tick”.

// Simple handshake: req high, then gnt one cycle later, then !req one cycle after that
req ##1 gnt ##1 !req

// Two clock tick gap: req now, gnt on the second subsequent tick
req ##2 gnt
// Equivalent: req ##1 'true ##1 gnt  ('true is always-true placeholder)

// Nth cycle check
a ##N b   // b must be true on the Nth clock tick after a is true

// Overlapped concatenation: c and d must be true at the SAME clock tick
// (a ##1 b ##1 c) ##0 (d ##1 e ##1 f)
// Equivalent to: a ##1 b ##1 (c && d) ##1 e ##1 f

// Delay ##0 a means: a must be true NOW (same tick as context)
// Delay ##1 a means: 'true ##1 a (skip one tick, then check a)
// Delay ##2 a means: 'true ##1 'true ##1 a (skip two ticks)

📋 Range Delays and ‘true

// Range delay: gnt must be true somewhere in the window [4, 32] after req
req ##[4:32] gnt

// Unbounded range: gnt must eventually be true (4 or more ticks after req)
req ##[4:$] gnt   // $ = finite but unbounded (end-of-sim or arbitrary)

// 'true: always evaluates to true — used as a placeholder for "skip a tick"
// Defined as:  'define true 1

// Range expansion — ##[0:3] a is equivalent to:
// a  OR  ('true ##1 a)  OR  ('true ##1 'true ##1 a)  OR  ('true ##1 'true ##1 'true ##1 a)

// Unconditional extension: a ##1 b ##1 c ##3 'true
// After c matches, the sequence extends 3 more ticks (for alignment)
a ##1 b ##1 c ##3 'true

📄 Declaring Named Sequences

Sequences can be named for reuse and parameterisation. A named sequence can be instantiated inside other sequences or properties by referencing its name.

// Simple named sequence — clock specified inside
sequence s1;
  @(posedge clk) a ##1 b ##1 c;
endsequence

// Named sequence with no clock — inherits from context
sequence s20_1(data, en);
  (!frame && (data == data_bus)) ##1 (c_be[0:3] == en);
endsequence
// When used in assert or property, the clock is inherited

// Composing: use s (a ##1 b ##1 c) inside a larger sequence
sequence s;  a ##1 b ##1 c;  endsequence

sequence rule;
  @(posedge sysclk)
  trans ##1 start_trans ##1 s ##1 end_trans;
endsequence
// Equivalent to: trans ##1 start_trans ##1 a ##1 b ##1 c ##1 end_trans

// Where sequences can be declared:
// module, interface, program, clocking block, package, compilation-unit scope

// Closing name (optional)
sequence abc;
  a ##1 b ##1 c;
endsequence : abc

📋 Composing Sequences

When a named sequence is used as a subsequence, it is expanded inline with actual arguments substituted for formals. Evaluation starts at the clock tick at which the reference is reached.

// Named sequence with argument
sequence e2(a, b, c);
  @(posedge sysclk) $rose(a) ##1 b ##1 c;
endsequence

sequence rule2;
  @(posedge sysclk)
  reset ##1 inst ##1 e2(ready, proc1, proc2).ended ##1 branch_back;
endsequence
// e2.ended: detects that e2 has completed, regardless of when it started

⛔ Cyclic Dependencies — Illegal

// ILLEGAL: s1 references s2, s2 references s1 → cycle
sequence s1; @(posedge sysclk) (x ##1 s2); endsequence
sequence s2; @(posedge sysclk) (y ##1 s1); endsequence
// Any syntactic cyclic dependency of sequence names is disallowed.

📋 Operator Precedence

🔄 Repetition Operators — Overview

📋 Consecutive Repetition [*]

// Exact repetition: b must be true on 3 consecutive ticks
a ##1 b [*3] ##1 c
// Equivalent: a ##1 b ##1 b ##1 b ##1 c

// Sequence repetition: (a ##2 b) repeated 5 times
(a ##2 b) [*5]
// = (a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b ##1 a ##2 b)

// Range repetition: b repeated 1 to 5 times
(a ##2 b) [*1:5]
// Matches if any of [*1], [*2], [*3], [*4], or [*5] matches

// Zero repetition: empty sequence
// b [*0] produces no match over any positive clock count
// Rules for empty sequence concatenation:
// (empty ##0 seq) → no match
// (empty ##n seq), n>0 → equivalent to ##(n-1) seq
b ##1 a[*0:1] ##2 c
// = (b ##2 c) OR (b ##1 a ##2 c)

// Unbounded: b must hold for any finite (≥1) number of ticks
a ##1 b [*1:$] ##1 c
// a is true, then b holds for ≥1 consecutive ticks, then c is true

// Delay with repetition (both directions)
'true ##3 (a [*3])
// means: 'true ##1 'true ##1 'true ##1 a ##1 a ##1 a
('true ##2 a) [*3]
// means: delay 2, a, delay 2, a, delay 2, a (6 ticks gap between each a)

📋 Goto Repetition [->]

Goto repetition matches a boolean expression exactly N times at non-consecutive clock ticks, with no match of the expression strictly between each matched pair. The sequence ends at the last matched tick.

// b must be true on exactly 2 to 10 non-consecutive ticks between a and c
// c must follow immediately after the last b tick
a ##1 b [->2:10] ##1 c

// Equivalent expansion:
a ##1 ((!b[*0:$] ##1 b) [*2:10]) ##1 c
// The key: no match of b strictly between consecutive matched ticks
// The sequence ENDS at the last b tick — c starts immediately after

// Practical example: ACK must arrive 1 to 3 cycles after REQ, then bus is released
// (no second ACK between two successive ACKs)
req ##1 ack [->1:3] ##1 !req

📋 Non-Consecutive Repetition [=]

Like goto repetition but the sequence can extend past the last matched tick by arbitrarily many ticks — as long as the expression is false on those extra ticks. The sequence ends at or after the last matched tick (but before any later match).

// b must be true exactly 2 to 10 non-consecutive ticks between a and c
// c does NOT have to follow immediately after the last b tick
// Any number of false-b ticks are allowed between last b and c
a ##1 b [=2:10] ##1 c

// Equivalent expansion:
a ##1 ((!b[*0:$] ##1 b) [*2:10]) ##1 !b[*0:$] ##1 c

// Difference from goto: goto ends exactly at the last b tick,
// non-consecutive can end any number of ticks after (while b stays false)

📋 Sampled Value Functions

These five system functions access sampled values for use in assertion expressions and procedural code. The clocking event is either explicit or inferred from context.

// $rose, $fell, $stable in always blocks
always @(posedge clk)
  reg1 <= a & $rose(b);       // true if b's LSB just changed to 1

always @(posedge clk)
  reg2 <= a & $past(b);       // uses b from the PREVIOUS posedge clk

// $past with gating and two ticks back
// Samples q only when enable was true at those past clock ticks
always @(posedge clk)
  assert (done |=> (out == $past(q, 2, enable)));
// Samples q 2 ticks back using posedge clk iff enable

// $fell example in assertion
assert property (@(posedge mclk) $fell(ack) |-> req);

& and — Both Must Match

The and operator requires both operand sequences to match, starting from the same clock tick. The overall match ends at the later of the two endpoint times.

// Both operands must match; end time = whichever finishes last
(te1 ##2 te2) and (te3 ##2 te4 ##2 te5)
// First operand ends at tick 10; second at tick 12 → match at tick 12

// With range: multiple matches possible
// (te1 ##[1:5] te2) and (te3 ##2 te4 ##2 te5)
// First operand: 5 possible end times (ticks 9,10,11,12,13)
// Second operand: ends at tick 12 (one match)
// Composite: 5 matches — 4 ending at tick 12, one at tick 13

// When both operands are simple boolean expressions:
// te1 and te2 matches if BOTH are true at the same tick

∩ intersect — Same Length

intersect requires both operands to match and their matches must have the same length. Only pairs of equal-length matches are combined.

// Stricter than and: only matches of the SAME length are paired
(te1 ##[1:5] te2) intersect (te3 ##2 te4 ##2 te5)
// Second operand always ends at tick 12 (length 4 ticks)
// Of the 5 possible first operand matches, only [*4] also ends at tick 12
// Result: exactly 1 match at tick 12 (unlike 'and' which gives 5)

// Formal equivalence: exp throughout seq  =  (exp)[*0:$] intersect seq
// throughout is intersect with the condition replicated at every tick

∨ or — Either Must Match

The or operator matches if at least one of the two operand sequences matches. All matches of either operand contribute independently to the composite match.

// Boolean expressions: te1 or te2 matches on any tick where at least one is true

// Sequences: union of all matches from both operands
(te1 ##2 te2) or (te3 ##2 te4 ##2 te5)
// First matches at tick 10, second at tick 12 → two composite matches

// With range: many more matches possible
// (te1 ##[1:5] te2) or (te3 ##2 te4 ##2 te5)
// First: matches at ticks 9, 10, 11, 12, 13
// Second: matches at tick 12
// Composite: ticks 9,10,11,13 have one match each; tick 12 has two matches

📌 first_match

first_match(seq) discards all but the earliest-ending match of seq. When used as a sub-sequence, it avoids ambiguity from range delays, reducing the number of parallel evaluation threads.

// te1 ##[2:5] te2 can produce 4 matches (at different end times)
// first_match takes only the earliest-ending one
sequence ts1;
  first_match(te1 ##[2:5] te2);
endsequence
// If te1 and te2 are expressions, only the match with ##2 (smallest gap) is kept

// Multiple sequences with the same earliest end time: ALL are kept
// first_match((a ##2 b) or (c ##2 d))
// If both match at the same tick, both are returned

// Attaching a local variable assignment to first_match
first_match(seq, x = e)   // equivalent to first_match((seq, x = e))

⊕ throughout — Condition Over a Span

expr throughout seq requires that expr is true at every clock tick throughout the match of seq. It is equivalent to (expr)[*0:$] intersect seq.

// burst_mode must remain low throughout the 7-tick burst transfer
sequence burst_rule1;
  @(posedge mclk)
  $fell(burst_mode) ##0
  (!burst_mode) throughout (##2 ((trdy==0) && (irdy==0)) [*7]);
endsequence
// Fails if burst_mode goes high at any point during the 7-cycle burst
// Succeeds only if burst_mode remains 0 through tick 10 after the $fell tick

// General form: condition holds throughout the entire span of the subsequence
!err throughout (req ##[1:4] gnt)
// !err must be true on every tick from req through gnt

⊂ within — Containment

seq1 within seq2 requires that seq2 matches over some interval and seq1 matches within a sub-interval of that same interval. It is equivalent to (1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2.

// seq1's match must be fully contained inside seq2's match
// Start of seq1 >= start of seq2; end of seq1 <= end of seq2
!trdy[*7] within (($fell(irdy) ##1 !irdy[*8]))
// trdy must be low for 7 consecutive ticks somewhere inside
// the 8-tick window starting with the falling edge of irdy

📌 ended — Endpoint Detection

The .ended method on a sequence instance returns true at any tick where the sequence has reached its endpoint, regardless of when that match started. This lets you use a named sequence as a condition without constraining when it started.

// Without .ended: e1 must START one tick after inst
sequence rule_no_ended;
  @(posedge sysclk)
  reset ##1 inst ##1 e1 ##1 branch_back;
endsequence

// With .ended: e1 can have started at ANY earlier tick, as long as it ENDS here
sequence e1;
  @(posedge sysclk) $rose(ready) ##1 proc1 ##1 proc2;
endsequence

sequence rule_ended;
  @(posedge sysclk)
  reset ##1 inst ##1 e1.ended ##1 branch_back;
endsequence

// .ended also works with parameterised sequences
e2(ready, proc1, proc2).ended

📌 Local Variables in Sequences

Sequences can declare local variables — dynamically allocated per evaluation attempt — for capturing and carrying data across a multi-cycle match. This avoids needing static variables which would be shared across overlapping checks.

// Pipeline latency check: capture pipe_in when valid_in, verify pipe_out 5 ticks later
property e;
  int x;
  (valid_in, (x = pipe_in)) |-> ##5 (pipe_out1 == (x+1));
endproperty
// x is captured when valid_in is true; compared 5 ticks later

// Data coherency check in a sequence
sequence data_check;
  int x;
  a ##1 !a, x = data_in ##1 !b[*0:$] ##1 b && (data_out == x);
endsequence
// x captures data_in when a falls; verified when b eventually rises

// Accumulation across repeated matches
sequence rep_v;
  int x;
  'true, x = 0 ##0
  (!a [*0:$] ##1 a, x = x+data) [*4] ##1 b ##1 c && (data_out == x);
endsequence
// x accumulates data across 4 occurrences of 'a'; checked against data_out

Visibility rules

• Local variables are not visible in the parent sequence when a named subsequence is instantiated.
• To share a local variable between sequences, pass it as a formal argument to the subsequence.
• A local variable cannot be declared with the same name as a formal argument of the same sequence.
• With or/and/intersect, local variables assigned on one thread are not visible in sibling threads. Only variables that flow out of all paths of an or are visible after the or.

// ILLEGAL: v1 not visible outside sub_seq1
sequence sub_seq1;
  int v1;
  a ##1 !a, v1 = data_in ##1 (data_out == v1);
endsequence
sequence seq1;
  c ##1 sub_seq1 ##1 (do1 == v1);  // ERROR: v1 not in scope
endsequence

// LEGAL: pass v1 as a formal argument
sequence sub_seq2(lv);
  a ##1 !a, lv = data_in ##1 (data_out == lv);
endsequence
sequence seq2;
  int v1;
  c ##1 sub_seq2(v1) ##1 (do1 == v1); // v1 bound to lv — legal
endsequence

▶ Subroutine Calls on Match

Tasks, void functions, and system tasks can be called at the endpoint of a sequence match by appending them (comma-separated) in parentheses alongside the terminal expression.

// $display is called at every match of the sequence
sequence s1;
  logic v, w;
  (a, v = e) ##1
  (b[->1], w = f, $display("b after a: v=%h w=%h", v, w));
endsequence
// At the match of b[->1]: w is assigned, then $display is called
// v and w have their current (just-assigned) values when $display runs

// Subroutine calls on first_match
first_match(seq, x = e)
// x is assigned at the first match, not all possible matches

• All subroutine calls attached to a sequence execute at every successful match.
• Within a match, calls execute in declaration order.
• Calls are scheduled in the Reactive region, like assertion action blocks.
• Arguments can be passed by value (using sampled values) or by ref/const ref.
• Local variables flowing out of the sequence can be used as actual arguments.

📌 Assertion System Functions

Four system functions simplify common assertion checks on bit vectors. All return bit (0 or 1).

// $onehot: exactly one bit is 1
assert property (@(posedge clk) $onehot(grant));
// grant is one-hot at every clock tick

// $onehot0: at most one bit is 1 (zero or one)
assert property (@(posedge clk) $onehot0(req));
// At most one request can be active

// $isunknown: any bit is X or Z
assert property (@(posedge clk) !$isunknown(data));
// data must never contain X or Z
// Equivalent to: !(^data === 'bx)

// $countones: count the number of 1 bits (returns int, X/Z not counted)
assert property (@(posedge clk) $countones(req) <= 2);
// No more than two requests active simultaneously

// Combining: exactly one bit set AND not unknown
assert property (@(posedge clk)
  !$isunknown(grant) && $onehot(grant));

📋 Quick Reference

Concatenation and delay forms

Repetition operators

Combination operators