Assertion Based Verification

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

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

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

2. ssr

September 20, 2016 at 10:54 am

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?

• September 20, 2016 at 7:12 pm

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

3. Av

December 6, 2018 at 2:33 pm

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

i.e, a sequence that perform like this:

req ##(counting_register_threshold) ack

### Most Popular

VLSI Pro is a professional network of VLSI engineers. Here you can find latest news, helpful articles and more on VLSI technology.