SystemVerilog Assertions with time delay

The examples in SystemVerilog Concurrent Assertions checked simple boolean expressions on every single clock edge. But sequential checks take several clock cycles to complete, and the time delay between two parts of a sequence is specified with the ## operator.

12 min read | Intermediate Level

What You'll Learn

• What the ## operator means inside a sequence, and how it differs from a plain boolean check
• Why a fresh attempt at the sequence starts on every clock edge, resulting in several overlapping instances tracked in parallel
• How to read a "started at Xns, failed/passed at Yns" log message for one specific pipelined instance
• Why a sequence's outcome for a given attempt is only known some cycles after it starts, not immediately

The ## Operator

If a is not high on a given clock cycle, that attempt at the sequence starts and fails on the very same cycle. But if a is high, the attempt starts and succeeds if b is high exactly 2 clocks later — it fails if b is low 2 clocks later instead:

module tb;
  bit a, b;
  bit clk;
  
  // This is a sequence that says 'b' should be high 2 clocks after
  // 'a' is found high. The sequence is checked on every positive
  // edge of the clock which ultimately ends up having multiple
  // assertions running in parallel since they all span for more
  // than a single clock cycle.
  sequence s_ab;
    @(posedge clk) a ##2 b;
  endsequence
  
  // Print a display statement if the assertion passed
  assert property(s_ab)
  	$display ("[%0t] Assertion passed !", $time);
  
  always #10 clk = ~clk;
  
  initial begin
    for (int i = 0; i < 10; i++) begin
      @(posedge clk);
      a <= $random;
      b <= $random;  
  
      $display("[%0t] a=%b b=%b", $time, a, b);
    end
  
    #20 $finish;
  end
endmodule

Multiple Instances Run in Parallel

Since the assertion is checked on every clock edge, a brand-new attempt at s_ab begins each time — and since each attempt takes 2 full cycles to resolve, several attempts end up "in flight" at once, each independently tracked from its own starting point:

Walking through two specific instances end to end makes the pattern concrete:

• At 50ns, a=1, so an attempt starts there. It needs b=1 two edges later, at 90ns — but b=0 at 90ns, so this specific attempt fails, reported on the 90ns row as FAIL (Start@50, Fail@90).
• At 70ns, a separate attempt starts (a=1 again). It needs b=1 at 110ns — and b=1 there, so this attempt passes, reported on the 110ns row as PASS (Start@70, Pass@110).

Notice these two attempts overlap in time — the one started at 50ns is still unresolved when the one at 70ns begins, and both are being tracked simultaneously. Each row in the table can carry two separate pieces of information: whether a new attempt starts on that exact edge, and whether some earlier attempt happens to resolve on that same edge.

Output

Compiler version P-2019.06-1; Runtime version P-2019.06-1;  Jan 16 06:49 2020
[10] a=0 b=0
"testbench.sv", 14: tb.unnamed$$_0: started at 10ns failed at 10ns
	Offending 'a'
[30] a=0 b=1
"testbench.sv", 14: tb.unnamed$$_0: started at 30ns failed at 30ns
	Offending 'a'
[50] a=1 b=1
[70] a=1 b=1
[90] a=1 b=0
"testbench.sv", 14: tb.unnamed$$_0: started at 50ns failed at 90ns
	Offending 'b'
[110] a=1 b=1
[110] Assertion passed !
[130] a=0 b=1
"testbench.sv", 14: tb.unnamed$$_0: started at 130ns failed at 130ns
	Offending 'a'
[130] Assertion passed !
[150] a=1 b=0
"testbench.sv", 14: tb.unnamed$$_0: started at 110ns failed at 150ns
	Offending 'b'
[170] a=1 b=0
[190] a=1 b=0
"testbench.sv", 14: tb.unnamed$$_0: started at 150ns failed at 190ns
	Offending 'b'
$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

Each log line names exactly which attempt it's reporting on, by its own start time — "started at 50ns failed at 90ns" is the same attempt traced above, and "started at 130ns failed at 130ns" is a brand-new attempt failing immediately because a=0 right at its own start.

Common Beginner Mistakes