FVO — Formal Verification Online
Lesson 3.4 · SystemVerilog Assertions Essentials

Sequences: describing behaviour over time

A sequence is a pattern of Boolean expressions over consecutive clock ticks. Sequences are the building blocks of properties.

Cycle delays: ##n and ##[m:n]

SequenceMeaning
a ##1 ba, then b on the next tick
a ##0 ba and b on the same tick (sequence fusion)
a ##3 ba, then b exactly 3 ticks later
a ##[1:4] ba, then b 1 to 4 ticks later
a ##[2:$] ba, then b at least 2 ticks later (unbounded)
0123456startmatchclkstartdone
start ##[1:4] done matches: start at cycle 1, done at cycle 4 (3 ticks later, within 1..4).

Repetition

OperatorNameMeaningExample
b[*3]consecutiveb on 3 consecutive ticksbusy[*3]
b[*2:4]consecutive rangeb on 2 to 4 consecutive ticksreq[*1:8]
b[->2]gotob true twice (not necessarily consecutive); ends on the 2nd back[->2]
b[=2]non-consecutiveLike goto, but the match may extend past the 2nd b while b is falseretry[=2]
01234567cmd2nd beatclkcmdbeat
cmd ##1 beat[->2] — after cmd, wait for the second beat (cycles 2 and 4). The sequence ends exactly at cycle 4.

Combining sequences

OperatorMeaning
s1 and s2Both match, starting together; may end at different times (ends at the later one)
s1 intersect s2Both match, starting and ending together
s1 or s2At least one matches
e throughout sBoolean e holds on every tick while s matches
s1 within s2s1 matches somewhere inside a match of s2
first_match(s)Only the earliest match of s is kept
named sequence
// A burst: 'busy' must stay high from start until done, which comes within 2..6 ticks
sequence s_burst;
  start ##1 (busy throughout (##[1:5] done));
endsequence

c_burst: cover property (@(posedge clk) s_burst);
Was this page helpful?

Tip: select any text on the page before clicking Report and it will be quoted in your report.