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

Click to execute on   

SystemVerilog assertion sequence
SystemVerilog assertion sequence

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

Click to execute 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

Click to execute on   

assertion sequence
assertion sequence

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

Click to execute 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);

Click to execute on   

❮ Previous Next ❯