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.

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.

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.

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

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

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.

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

eg: A sequence can be referenced in a sequence

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

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.

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.

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

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):
Positional association (with defaults):

Default value 1 will be taken for sig3

Named association (with default):

Default value 1 will be taken for sig3

Named association (without default):

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

Sini Balakrishnan

Sini Balakrishnan

Staff Engineer at Intel
Sini has spent more than a dozen years in the semiconductor industry, focusing mostly on verification. She is an expert on Formal Verification and has written international papers and articles on related topics.
Sini Balakrishnan

Latest posts by Sini Balakrishnan (see all)

3 Comments

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

Leave a Reply

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