Contact / Report an issue

SystemVerilog assertion Sequence

SVA Sequence


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

Execute the above code on 


assertion sequence
SystemVerilog assertion sequence
* click on image for a better view

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

Execute the above code on 

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

Execute the above code on 

Assertion sequence
assertion sequence
* click on image for a better view

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

Execute the above code on 

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

Execute the above code on