SVA Sequence
Table of Contents
Boolean expression events that evaluate over a period of time involving single/multiple clock cycles. SVA provides a keyword to represent these events called “sequence”.
SVA Sequence example
In the below example the sequence seq_1 checks that the signal “a” is high on every positive edge of the clock. If the signal “a” is not high on any positive clock edge, the assertion will fail.
sequence seq_1; @(posedge clk) a==1; endsequence
A sequence with a logical relationship
Below sequence, seq_2 checks that on every positive edge of the clock, either signal “a” or signal “b” is high. If both the signals are low, the assertion will fail.
sequence seq_2; @(posedge clk) a || b; endsequence
Sequence Expressions
By defining arguments in a sequence definition, the same sequence can be re-used for similar behavior.
For example, we can define a sequence as below.
sequence seq_lib (a, b) a || b ; endsequence
this seq can be used as,
sequence s_lib_inst seq_lib(req1,req2); endsequence
Sequences with timing relationship
In SVA, clock cycle delays are represented by a “##” sign. For example, ##2 means 2 clock cycles.
Below sequence checks for the signal “a” being high on a given positive edge of the clock. If the signal “a” is not high, then the sequence fails. If signal “a” is high on any given positive edge of the clock, the signal “b” should be high 2 clock cycles after that. If signal “b” is not asserted after 2 clock cycles, the assertion fails.
sequence seq; @(posedge clk) a ##2 b; endsequence
Note:: sequence begins when signal “a” is high on a positive edge of the clock.
Clock usage in SVA
A clock can be specified in a sequence, in a property or even in an assert statement.
Clock defined in the sequence definition
The previous example shows the usage of a clock inside the sequence definition.
sequence seq; @(posedge clk) a ##2 b; endsequence
Clock defined in the property definition
sequence seq; a ##2 b; endsequence property p; @(posedge clk) seq; endproperty a_1 : assert property(p);
In general, it is a good idea to define the clocks in property definitions and keep the sequences independent of the clocks. This will help increase the re-use of the basic sequence definitions.
Forbidding a property
A separate property definition is not needed to assert a sequence. the expression to be checked can be called from the assert statement directly as shown below.
In all the examples shown so far, the property is checking for a true condition. we expect the property to be false always. If the property is true, the assertion fails.
sequence seq;
a ##2 b;
endsequence
a_2: assert property(@(posedge clk) seq);
Calling a property with a clock definition from within the assert statement is not allowed.
a_3: assert property(@(posedge clk) p) ; //Not allowed
Below sequence checks that if signal “a” is high on a given positive edge of the clock, then after 2 clock cycles, signal “b” shall not be high. The keyword “not” is used to specify that the property should never be true.
sequence seq; @(posedge clk) a ##2 b; endsequence property p; not seq; endproperty a_1: assert property(p);