Sequence in Assertions

The series or expressions spread over one or more clock cycles is called a sequence. A complex property can be phrased with multiple sequence blocks. Sequences are constructed over SystemVerilog boolean expressions. If an expression is evaluated correctly, a sequence is said to be matched. These expressions evaluate over a period of time that may involve one or more clock cycles.
The sequence feature provides the capability to manipulate and build sequential behavior.
The property checks for one or more SystemVerilog sequences. The evaluation of sequence involves a search for a match of the sequence beginning at a particular clock tick.
The clock cycle delay is specified using ## from the end of the first sequence till the start of the second sequence.
If a clocking event is not specified, then clocking will be inferred from the property from where it is called.
A sequence can be declared in the interface, clocking block, program, module, and package.

Syntax:

sequence <sequence_name>;
  <expression>;
endsequence

Linear sequence

A finite list of SystemVerilog boolean expressions in the linear order of increasing time is known as a linear sequence. The linear sequence is said to be matched when the first expression evaluates true followed by finite consecutive clock ticks, then the second expression evaluates true followed by finite consecutive clock ticks, and so on till the last expression evaluates true.

SVA sequence examples

The sequence with timing relationship

module assertion_example;
  bit clk, req1, req2;
  
  always #2 clk = ~clk;
  
  sequence seq;
    req1 ##5 req2;
  endsequence
  
  property prop;
    @(posedge clk) seq;
  endproperty
  
  time_a: assert property(prop);
    
  initial begin
    $dumpfile("dump.vcd");
    $dumpvars;
    
    req1 = 0;
    req2 = 0;
    
    #4 req1 = 1;
    req2 = 1;
    #6 req1 = 0;
    #6 req2 = 0;
    #10 req1 = 1;
    #20 req2 = 1;
    #20; $finish;
  end
endmodule

Output:

    req1 ##5 req2;
       |
xmsim: *E,ASRTST (./testbench.sv,16): (time 2 NS) Assertion assertion_example.time_a has failed (1 cycles, starting 2 NS)
    req1 ##5 req2;
       |
xmsim: *E,ASRTST (./testbench.sv,16): (time 14 NS) Assertion assertion_example.time_a has failed (1 cycles, starting 14 NS)
    req1 ##5 req2;
       |
xmsim: *E,ASRTST (./testbench.sv,16): (time 18 NS) Assertion assertion_example.time_a has failed (1 cycles, starting 18 NS)
    req1 ##5 req2;
       |
xmsim: *E,ASRTST (./testbench.sv,16): (time 22 NS) Assertion assertion_example.time_a has failed (1 cycles, starting 22 NS)
    req1 ##5 req2;
                |
xmsim: *E,ASRTST (./testbench.sv,16): (time 26 NS) Assertion assertion_example.time_a has failed (6 cycles, starting 6 NS)
    req1 ##5 req2;
       |
xmsim: *E,ASRTST (./testbench.sv,16): (time 26 NS) Assertion assertion_example.time_a has failed (1 cycles, starting 26 NS)
    req1 ##5 req2;
                |
xmsim: *E,ASRTST (./testbench.sv,16): (time 30 NS) Assertion assertion_example.time_a has failed (6 cycles, starting 10 NS)
Simulation complete via $finish(1) at time 66 NS + 0

The sequence with a logical expression

module assertion_example;
  bit clk, req1, req2;
  
  always #2 clk = ~clk;
  
  sequence seq;
    req1 && req2;
  endsequence
  
  property prop;
    @(posedge clk) seq;
  endproperty
  
  logical_exp: assert property(prop);
    
  initial begin
    $dumpfile("dump.vcd");
    $dumpvars;
    
    req1 = 0;
    req2 = 0;
    
    #4 req1 = 1;
    req2 = 1;
    #6 req1 = 0;
    #6 req2 = 0;
    #10 req1 = 1;
    #20 req2 = 1;
    #20; $finish;
  end
endmodule

Output:

xmsim: *E,ASRTST (./testbench.sv,16): (time 2 NS) Assertion assertion_example.logical_exp has failed 
xmsim: *E,ASRTST (./testbench.sv,16): (time 14 NS) Assertion assertion_example.logical_exp has failed 
Simulation complete via $finish(1) at time 66 NS + 0

The sequence with a formal argument

module assertion_example;
  bit clk, req1, req2, en;
  
  always #2 clk = ~clk;
  
  sequence seq(en);
    (req1 | req2) & en;
  endsequence
  
  property prop(en);
    @(posedge clk) seq(en);
  endproperty
  
  logical_exp: assert property(prop(en));
    
  initial begin
    $dumpfile("dump.vcd");
    $dumpvars;
    
    req1 = 0;
    req2 = 0;
    
    #4 req1 = 1;
    #4 req2 = 1;
    #6 req1 = 0;
    #6 req2 = 0;
    en = 1;
    #10 req1 = 1;
    #20 req2 = 1;
    #20; $finish;
  end
endmodule

Output:

xmsim: *E,ASRTST (./testbench.sv,16): (time 2 NS) Assertion assertion_example.logical_exp has failed 
Simulation complete via $finish(1) at time 70 NS + 0

Multiple sequences example

module assertion_example;
  bit clk, req1, req2;
  
  always #2 clk = ~clk;
  
  sequence seqA;
    req1 ##5 req2;
  endsequence
  
  sequence seqB;
    req1 && req2;
  endsequence
  
  property prop;
    @(posedge clk) seqA |-> seqB;
  endproperty
  
  time_a: assert property(prop) $info("assertion passed"); else $error("assertion failed");
    
  initial begin
    $dumpfile("dump.vcd");
    $dumpvars;
    
    req1 = 0;
    req2 = 0;
    
    #4 req1 = 1;
    req2 = 1;
    #6 req1 = 0;
    #6 req2 = 0;
    #10 req1 = 1;
    #20 req2 = 1;
    #20; $finish;
  end
endmodule

Output:

xmsim: *N,ASRTST (./testbench.sv,20): (time 50 NS) Assertion assertion_example.time_a has passed
assertion passed
xmsim: *N,ASRTST (./testbench.sv,20): (time 54 NS) Assertion assertion_example.time_a has passed
assertion passed
xmsim: *N,ASRTST (./testbench.sv,20): (time 58 NS) Assertion assertion_example.time_a has passed
assertion passed
xmsim: *N,ASRTST (./testbench.sv,20): (time 62 NS) Assertion assertion_example.time_a has passed
assertion passed
Simulation complete via $finish(1) at time 66 NS + 0

Empty sequence

A sequence that does not match over any positive number of clock cycles is called an empty sequence.

Example

req[*0]: This means it does not repeat for any positive number of clock cycles.

Simplify below event sequence

Sequence

req1 ##3 req2 ##1 req1 ##3 req2 ##1 req1 ##3 req2

req1[*0:2] ##1 req2

Sequence Simplification

(req1 ##3 req2)[*3];

req2 //or
req1 ##1 req2 //or
req1 ##1 req1 ##1 req2