SVA Sequences I : 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.
sequence_expr ::= cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } | sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr } | expression_or_dist [ boolean_abbrev ] | sequence_instance [ sequence_abbrev ] | ( sequence_expr {, sequence_match_item } ) [ sequence_abbrev ] | sequence_expr and sequence_expr | sequence_expr intersect sequence_expr | sequence_expr or sequence_expr | first_match ( sequence_expr {, sequence_match_item} ) | expression_or_dist throughout sequence_expr | sequence_expr within sequence_expr | clocking_event sequence_expr cycle_delay_range ::=
constant_primary
| ## [ cycle_delay_const_range_expression ] | ##[*] | ##[+] sequence_match_item ::= operator_assignment | inc_or_dec_expression | subroutine_call sequence_instance ::= ps_or_hierarchical_sequence_identifier [ ( [ sequence_list_of_arguments ] ) ] sequence_list_of_arguments ::= [sequence_actual_arg] { , [sequence_actual_arg] } { , . identifier ( [sequence_actual_arg] ) } | . identifier ( [sequence_actual_arg] ) { , . identifier ( [sequence_actual_arg] ) } sequence_actual_arg ::= event_expression | sequence_expr boolean_abbrev ::= consecutive_repetition | non_consecutive_repetition | goto_repetition sequence_abbrev ::= consecutive_repetition consecutive_repetition ::= [* const_or_range_expression ] | [*] | [+] non_consecutive_repetition ::= [= const_or_range_expression ] goto_repetition ::= [-> const_or_range_expression ] const_or_range_expression ::= constant_expression | cycle_delay_const_range_expression cycle_delay_const_range_expression ::= constant_expression : constant_expression | constant_expression : $ expression_or_dist ::= expression [ dist { dist_list } ]
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 my_seq; req ##1 ack; endsequence: my_seq
property my_prop; @(posedge clk) disable iff (rst) my_seq |=> (out == in1 and in2); endproperty : prop
eg: A sequence can be referenced in a sequence
sequence my_seq; req ##1 ack; endsequence: my_seq
sequence out_seq; my_seq ##2 out1 ##1 out2; endsequence: out_seq
eg: A sequence can be referenced in an assert, assume, cover, or restrict statement.
sequence my_seq; req ##1 ack; endsequence: my_seq
assert property (@(posedge clk) my_seq); cover property (@(posedge clk) my_seq); assume property (@(posedge clk) my_seq); restrict property (@(posedge clk) my_seq);
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
- sequence_expr
- event_expression
- terminal $ in a cycle_delay_const_range_expression
With typed arguments
A formal argument may be typed by specifying the type prior to the formal_port_identifier 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 my_seq1; s1 ##1 s2 ##2 s3; endsequence: my_seq1
sequence my_seq2 (sequence seq,expr, shortint cnt,bit sig,event myevent); //formal argument (typed) @(myevent) seq ##cnt expr ##[10:15] sig; endsequence: my_seq2
property prop; @(posedge clk) $changed(in) |-> my_seq2(my_seq1,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 formal_port_identifier in the port list. There is no default type for a formal argument.
In the following code, my_seq2 has formal untyped arguments seq,cnt,sig and expr.
sequence my_seq1; s1 ##1 s2 ##2 s3; endsequence: my_seq1
sequence my_seq2 (seq,cnt,sig,expr,myevent); //formal argument @(myevent) seq ##9 expr ##[10:cnt] sig; endsequence: my_seq2
property prop; @(posedge clk) $changed(in) |-> my_seq2(my_seq1,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".