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) | a | Result |
---|---|---|
10 | 0 | FAIL |
30 | 1 | PASS |
50 | 1 | PASS |
70 | 1 | PASS |
90 | 1 | PASS |
110 | 1 | PASS |
130 | 1 | PASS |
150 | 0 | FAIL |
170 | 1 | PASS |
190 | 1 | PASS |
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) | a | Transition | Result |
---|---|---|---|
10 | 0 | FAIL | |
30 | 1 | 0->1 | PASS |
50 | 1 | FAIL | |
70 | 1 | FAIL | |
90 | 1 | FAIL | |
110 | 1 | FAIL | |
130 | 1 | FAIL | |
150 | 0 | 1->0 | FAIL |
170 | 1 | 0->1 | PASS |
190 | 1 | FAIL |
The behavior is visible in the simulation log where assertion failed at all times other than 30ns and 170ns.
Simulation LogCompiler 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) | a | Transition | Result |
---|---|---|---|
10 | 0 | FAIL | |
30 | 1 | 0->1 | FAIL |
50 | 1 | FAIL | |
70 | 1 | FAIL | |
90 | 1 | FAIL | |
110 | 1 | FAIL | |
130 | 1 | FAIL | |
150 | 0 | 1->0 | PASS |
170 | 1 | 0->1 | FAIL |
190 | 1 | FAIL |
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) | a | Transition | Result |
---|---|---|---|
10 | 0 | FAIL | |
30 | 1 | 0->1 | FAIL |
50 | 1 | PASS | |
70 | 1 | PASS | |
90 | 1 | PASS | |
110 | 1 | PASS | |
130 | 1 | PASS | |
150 | 0 | 1->0 | FAIL |
170 | 1 | 0->1 | FAIL |
190 | 1 | PASS |
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