A sequence is a simple building block in SystemVerilog assertions that can represent certain expressions to aid in creating more complex properties.

Simple Sequence


module tb;
  	bit a;
  	bit clk;
  
	// This sequence states that a should be high on every posedge clk
  	sequence s_a;
      @(posedge clk) a;
    endsequence
  
  	// When the above sequence is asserted, the assertion fails if 'a'
  	// is found to be not high on any posedge clk
  	assert property(s_a);

      
	always #10 clk = ~clk;
      
	initial begin
      for (int i = 0; i < 10; i++) begin        
        a = $random;
        @(posedge clk);
        
        // Assertion is evaluated in the preponed region and 
        // use $display to see the value of 'a' in that region
        $display("[%0t] a=%0d", $time, a);
      end
      #20 $finish;
    end
endmodule
Time (ns)aResult
100FAIL
301PASS
501PASS
701PASS
901PASS
1101PASS
1301PASS
1500FAIL
1701PASS
1901PASS
 Simulation Log
Compiler version P-2019.06-1; Runtime version P-2019.06-1;  Jan 14 06:32 2020
[10] a=0
"testbench.sv", 12: tb.unnamed$$_0: started at 10ns failed at 10ns
	Offending 'a'
[30] a=1
[50] a=1
[70] a=1
[90] a=1
[110] a=1
[130] a=1
[150] a=0
"testbench.sv", 12: tb.unnamed$$_0: started at 150ns failed at 150ns
	Offending 'a'
[170] a=1
[190] a=1
$finish called from file "testbench.sv", line 27.
$finish at simulation time                  210
           V C S   S i m u l a t i o n   R e p o r t 
Time: 210 ns

$rose

The system task $rose is used to detect a positive edge of the given signal. In this case $rose of a indicates that a posedge of a is expected to be seen on every posedge of clk . Because SystemVerilog assertions evaluate in the preponed region, it can only detect value of the given signal in the preponed region. When value of the signal is 0 in the first edge and then 1 on the next edge, a positive edge is assumed to have happened. So, this requires 2 clocks to be identified.


module tb;
  	bit a;
  	bit clk;
  
	// This sequence states that 'a' should rise on every posedge clk
  	sequence s_a;
      @(posedge clk) $rose(a);
    endsequence
  
  	// When the above sequence is asserted, the assertion fails if 
  	// posedge 'a' is not found on every posedge clk
  	assert property(s_a);

      
	// Rest of the testbench stimulus
endmodule

See that a positive edge was detected and the assertion passed at 30ns in the image shown below. This is because value of a is 0 at 10ns and 1 at 30ns upon which the assertion completes and is proven to be successful.

Time (ns)aTransitionResult
100FAIL
3010->1PASS
501FAIL
701FAIL
901FAIL
1101FAIL
1301FAIL
15001->0FAIL
17010->1PASS
1901FAIL

The behavior is visible in the simulation log where assertion failed at all times other than 30ns and 170ns.

 Simulation Log
Compiler version P-2019.06-1; Runtime version P-2019.06-1;  Jan 14 06:58 2020
[10] a=0
"testbench.sv", 12: tb.unnamed$$_0: started at 10ns failed at 10ns
	Offending '$rose(a)'
[30] a=1
[50] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 50ns failed at 50ns
	Offending '$rose(a)'
[70] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 70ns failed at 70ns
	Offending '$rose(a)'
[90] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 90ns failed at 90ns
	Offending '$rose(a)'
[110] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 110ns failed at 110ns
	Offending '$rose(a)'
[130] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 130ns failed at 130ns
	Offending '$rose(a)'
[150] a=0
"testbench.sv", 12: tb.unnamed$$_0: started at 150ns failed at 150ns
	Offending '$rose(a)'
[170] a=1
[190] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 190ns failed at 190ns
	Offending '$rose(a)'
$finish called from file "testbench.sv", line 27.
$finish at simulation time                  210
           V C S   S i m u l a t i o n   R e p o r t 
Time: 210 ns

$fell

The system task $fell is used to detect negative edge of the given signal. In this case $fell of a indicates that a negedge of a is expected to be seen on every posedge of clk . Because SystemVerilog assertions evaluate in the preponed region, it can only detect value of the given signal in the preponed region. When value of the signal is 1 on the first edge and then 0 on the next edge, a negative edge is assumed to have happened. So, this requires 2 clocks to be identified.


module tb;
  	bit a;
  	bit clk;
  
	// This sequence states that 'a' should fall on every posedge clk
  	sequence s_a;
      @(posedge clk) $fell(a);
    endsequence
  
  	// When the above sequence is asserted, the assertion fails if 
  	// negedge 'a' is not found on every posedge clk
  	assert property(s_a);

      
	// Rest of the testbench stimulus
endmodule

See that a negative edge was detected and the assertion passed at 1500ns in the image shown below. This is because value of a is 1 at 130ns and 0 at 150ns upon which the assertion completes and is proven to be successful.

Time (ns)aTransitionResult
100FAIL
3010->1FAIL
501FAIL
701FAIL
901FAIL
1101FAIL
1301FAIL
15001->0PASS
17010->1FAIL
1901FAIL
 Simulation Log
Compiler version P-2019.06-1; Runtime version P-2019.06-1;  Jan 14 07:09 2020
[10] a=0
"testbench.sv", 12: tb.unnamed$$_0: started at 10ns failed at 10ns
	Offending '$fell(a)'
[30] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 30ns failed at 30ns
	Offending '$fell(a)'
[50] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 50ns failed at 50ns
	Offending '$fell(a)'
[70] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 70ns failed at 70ns
	Offending '$fell(a)'
[90] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 90ns failed at 90ns
	Offending '$fell(a)'
[110] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 110ns failed at 110ns
	Offending '$fell(a)'
[130] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 130ns failed at 130ns
	Offending '$fell(a)'
[150] a=0
[170] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 170ns failed at 170ns
	Offending '$fell(a)'
[190] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 190ns failed at 190ns
	Offending '$fell(a)'
$finish called from file "testbench.sv", line 27.
$finish at simulation time                  210
           V C S   S i m u l a t i o n   R e p o r t 
Time: 210 ns

$stable


module tb;
  	bit a;
  	bit clk;
  
	// This sequence states that 'a' should be stable on every clock
	// and should not have posedge/negedge at any posedge clk
  	sequence s_a;
      @(posedge clk) $stable(a);
    endsequence
  
  	// When the above sequence is asserted, the assertion fails if 
  	// 'a' toggles at any posedge clk
  	assert property(s_a);

      
	// Rest of the testbench stimulus
endmodule
Time (ns)aTransitionResult
100FAIL
3010->1FAIL
501PASS
701PASS
901PASS
1101PASS
1301PASS
15001->0FAIL
17010->1FAIL
1901PASS
 Simulation Log
Compiler version P-2019.06-1; Runtime version P-2019.06-1;  Jan 14 07:12 2020
[10] a=0
[30] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 30ns failed at 30ns
	Offending '$stable(a)'
[50] a=1
[70] a=1
[90] a=1
[110] a=1
[130] a=1
[150] a=0
"testbench.sv", 12: tb.unnamed$$_0: started at 150ns failed at 150ns
	Offending '$stable(a)'
[170] a=1
"testbench.sv", 12: tb.unnamed$$_0: started at 170ns failed at 170ns
	Offending '$stable(a)'
[190] a=1
$finish called from file "testbench.sv", line 27.
$finish at simulation time                  210
           V C S   S i m u l a t i o n   R e p o r t 
Time: 210 ns