Basics

Sequences

Sequence is a finite list of System Verilog Boolean expressions which matches along a finite interval of consecutive clock ticks. It evaluates Boolean expressions to true in each clock tick till the last expression. The major difference of sequence from a property is that, sequence does not have a success/fail status. Instead, it simply matches or not.

Following is a very simple sequence.

sequence seq1; a ##1 b ##1 c; endsequence: seq1

When signal 'a' goes high, the sequence will be under evaluation and checks for 'b' after 1 clock cycle. If there is a match on signal 'b' as well, value of 'c' will be evaluated after 1 clock cycle from 'b'. If there is a match in signal 'c', then sequence match is detected at the time-point where 'c' becomes 1.

Please have a look at the below waveform to get better clarity.

Here, signal 'a' goes high at time step 2, and 'b' goes high at time step 3 and 'c' at time step 4. So sequence shows a match at time step 4. Similarly 'a' goes high at time step 3 as well and signal 'b' at time step 4 and 'c' at time step 5. So, there is one match at time step 5. Rest all are shown as ‘no-match’.

Some of the features which you need to verify might have complex sequences. If you develop complex sequences, debugging would be difficult when it fails. So I always suggest to develop simple sequences. For writing complex sequence, use multiple simple sequences which helps in debugging and also helps others to understand your code well.

Sequence syntax is mentioned in LRM below.

sequenceexpr ::= cycledelayrange sequenceexpr { cycledelayrange sequenceexpr } | sequenceexpr cycledelayrange sequenceexpr { cycledelayrange sequenceexpr } | expressionordist [ booleanabbrev ] | sequenceinstance [ sequenceabbrev ] | ( sequenceexpr {, sequencematchitem } ) [ sequenceabbrev ] | sequenceexpr and sequenceexpr | sequenceexpr intersect sequenceexpr | sequenceexpr or sequenceexpr | firstmatch ( sequenceexpr {, sequencematchitem} ) | expressionordist throughout sequenceexpr | sequenceexpr within sequenceexpr | clockingevent sequenceexpr cycledelayrange ::=

constantprimary

| ## [ cycledelayconstrangeexpression ] | ##[*] | ##[+] sequencematchitem ::= operatorassignment | incordecexpression | subroutinecall sequenceinstance ::= psorhierarchicalsequenceidentifier [ ( [ sequencelistofarguments ] ) ] sequencelistofarguments ::= [sequenceactualarg] { , [sequenceactualarg] } { , . identifier ( [sequenceactualarg] ) } | . identifier ( [sequenceactualarg] ) { , . identifier ( [sequenceactualarg] ) } sequenceactualarg ::= eventexpression | sequenceexpr booleanabbrev ::= consecutiverepetition | nonconsecutiverepetition | gotorepetition sequenceabbrev ::= consecutiverepetition consecutiverepetition ::= [* constorrangeexpression ] | [*] | [+] nonconsecutiverepetition ::= [= constorrangeexpression ] gotorepetition ::= [-> constorrangeexpression ] constorrangeexpression ::= constantexpression | cycledelayconstrangeexpression cycledelayconstrangeexpression ::= constantexpression : constantexpression | constantexpression : $ expressionordist ::= expression [ dist { distlist } ]

Delay in Sequence

Delay -Fixed number of cycles

This is to specify the number of cycles to wait from one signal/sequence to the other.

e.g. 1: The signal b will be active after 1 clock cycle delay, once a is active.

sequence seq a ##1 b; endsequence seq

e.g. 2: After request is asserted, ack will be active 3 clock cycles later.

sequence seq @(posedge clk) req ##3 ack; endsequence seq

e.g. 3: seq1 followed by seq2 (joining two sequences)

sequence seq seq1 ##0 seq2; endsequence seq

Delay -Fixed range of cycles

Delay - Fixed Range This is to specify the number of cycles in a range to wait from one signal/sequence to the other. e.g. ##[expr1:expr2] The expressions in the range must be 0 or greater and must be static at compile time. Also note that, the expr2 must be greater than or equal to expr1.

e.g. After request is asserted, ack will be asserted within 1 to 4 clock cycles.

sequence seq @(posedge clk) req ##[1:4] ack; endsequence

This creates 4 evaluation threads which are req ##1 ack req ##2 ack req ##3 ack req ##4 ack

Interval of cycles – open ended

Open Ended delay sequence will try to match the sequence till end of simulation.

sequence seq req ##[1:$] ack endsequence seq

Sequence -Declaration & Instantiation

Declaration:

A sequence can be declared in:

• module
• interface
• program
• clocking block
• package
• compilation-unit scope
• checker
• generate block

Instantiate or Refer

A sequence can be referenced/instantiated in a property, sequence, assert, assume, cover, or restrict statement.

e.g. A sequence can be referenced in a property

sequence myseq; req ##1 ack; endsequence: myseq

property myprop; @(posedge clk) disable iff (rst) myseq |=> (out == in1 and in2); endproperty : prop

eg: A sequence can be referenced in a sequence

sequence myseq; req ##1 ack; endsequence: myseq

sequence outseq; myseq ##2 out1 ##1 out2; endsequence: outseq

eg: A sequence can be referenced in an assert, assume, cover, or restrict statement.

sequence myseq; req ##1 ack; endsequence: myseq

assert property (@(posedge clk) myseq); cover property (@(posedge clk) myseq); assume property (@(posedge clk) myseq); restrict property (@(posedge clk) myseq);

Sequences can have formal arguments in order to make sequences reusable. These are typed or untyped. Formal arguments are optional and can have default values.

A formal argument may be written in place of various syntactic entities, such as the following:

• identifier
• expression
• sequenceexpr
• eventexpression
• terminal $ in a cycledelayconstrangeexpression

With typed arguments

A formal argument may be typed by specifying the type prior to the formalportidentifier of the formal argument. A type shall apply to all formal arguments whose identifiers follow the type and precede the next type (if any) specified in the port list.

sequence myseq1; s1 ##1 s2 ##2 s3; endsequence: myseq1

sequence myseq2 (sequence seq,expr, shortint cnt,bit sig,event myevent); //formal argument (typed) @(myevent) seq ##cnt expr ##[10:15] sig; endsequence: myseq2

property prop; @(posedge clk) $changed(in) |-> myseq2(myseq1,5,x,==z^y,posedge clk); //actual argument endproperty: prop

assert property ( prop );

With untyped arguments

A formal argument is said to be untyped if there is no type specified prior to its formalportidentifier in the port list. There is no default type for a formal argument.

In the following code, myseq2 has formal untyped arguments seq,cnt,sig and expr.

sequence myseq1; s1 ##1 s2 ##2 s3; endsequence: myseq1

sequence myseq2 (seq,cnt,sig,expr,myevent); //formal argument @(myevent) seq ##9 expr ##[10:cnt] sig; endsequence: myseq2

property prop; @(posedge clk) $changed(in) |-> myseq2(myseq1,15,x,==z^y,posedge clk); //actual argument endproperty: prop

assert property ( prop );

The actual argument of an untyped formal argument can be anything so that its substitution results in a valid sequence.

The $ may be an actual argument in an instance of a named sequence, either declared as a default actual argument or passed in the list of arguments of the instance. If $ is an actual argument, then the corresponding formal argument shall be untyped.

Named or by positional association

sequence seq(sig1,sig2,sig3=1’b1); sig1 ##2 sig2 ##[3:5] sig3; endsequence: seq

In the above sequence seq sig1, sig2 and sig3 are the formal arguments. The argument sig3 has default value. This sequence can be referenced in a property in the following ways. Below code shows, how actual arguments of a sequence can be applied by named or by positional association.

Positional association (without default):

property prop; @(posedge clk) seq(x,y,z); endproperty: prop

Positional association (with defaults):

Default value 1 will be taken for sig3

property prop; @(posedge clk) seq(x,y); endproperty: prop

Named association (with default):

Default value 1 will be taken for sig3

property prop; @(posedge clk) seq(.sig1(x),.sig2(y)); endproperty: prop

Named association (without default):

property prop; @(posedge clk) seq(.sig1(x),.sig2(y), .sig3(z)); endproperty: prop

More about sequences can be found in other sections of "SVA Sequences".