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.
sva_sequence

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”.

4 comments on “SVA Sequences I : Basics

  1. Pingback: SVA Properties I : Basics | VLSI Pro

  2. ssr

    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

    What does line 8 mean?

    Reply
    1. Sini Balakrishnan Post author

      my_seq |=> (out == in1 and in2);
      If my_seq happens, check for the “out” in the next clock cycle and it should be in1 “AND” in2.
      Here, sequence is the antecedent of the property my_prop.
      Hope it is clear

      Reply
  3. Av

    There is a convinient way to perform dynamic delay in sequences?

    i.e, a sequence that perform like this:

    req ##(counting_register_threshold) ack

    Reply
  4. LK

    What does this line mean?  (or is it a typographical error)

    my_seq |=>

     

    This is shown in the section “Instantiate or Refer”, under the first example (the one marked “e.g. not eg”)

    Reply

Leave a Reply to LK Cancel reply

Your email address will not be published. Required fields are marked *