SystemVerilog assertion Sequence

 SVA Sequence 

Sequence seq_1 checks that the signal "a" is high on every positive edge of the clock. If 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 



Sequence with 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 the similar behavior.

For example, we can define a sequence as follows.

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 signal "a" is not high, then the sequence fails. If signal "a" is high on any given positive edge of clock, then 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 



Note :: sequence begins when signal "a" is high on a positive edge of the clock.

A clock can be specified in a sequence, in a property or even in an assert statement.
clock defined in the sequence definition:

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.

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.

 Forbidding a property 

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