Tutorials

Protocols

Learn More

Contents hide

1 Sequence in Assertions

1.1 What Is an SVA Sequence?

1.1.1 Where does the Clock Come From?

1.2 Linear sequence

1.3 SVA sequence examples

1.3.1 The sequence with timing relationship

1.3.2 The sequence with a logical expression

1.3.3 The sequence with a formal argument

1.3.4 Multiple sequences example

1.4 Empty sequence

1.5 Simplify below event sequence

1.6 Common Mistakes

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.

What Is an SVA Sequence?

Think of a sequence as a reusable timing pattern. The sequence itself describes when expressions must match; a property gives that pattern assertion meaning, and an assertion reports whether the property succeeds or fails.

Layer	Purpose	Small example
Boolean expression	Checks values at one sampled clock	req1 && req2
Sequence	Describes values across time	req1 ##5 req2
Property	Defines the rule and its clocking context	@(posedge clk) seq
Assertion	Evaluates the property and reports a result	assert property (prop);

Sequences can be declared in modules, interfaces, programs, packages, and clocking blocks. A named sequence is helpful when the same timing pattern is reused in several properties.

Syntax:

sequence <sequence_name>;
  <sequence_expression>;
endsequence
sequence req_to_ack;
  req ##2 ack;
endsequence

Code	Meaning
sequence req_to_ack	Begins a named sequence called req_to_ack
req	Must be true at the starting sampled clock
##2	Move forward by two sampled clock ticks
ack	Must be true at that later clock
endsequence	Ends the sequence declaration

Where does the Clock Come From?

A sequence may declare its own clock, or it may inherit the clock from the property that uses it. Keeping the clock in the property is common because one sequence can then be reused with a clear checking context.

sequence req_to_ack;
  req ##2 ack;
endsequence

property p_req_to_ack;
  @(posedge clk) req_to_ack;
endproperty

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.

The ## operator specifies the number of sampled clock ticks between the expressions; it does not represent simulation-time units such as nanoseconds.

Sequence expression	Timing meaning
a ##0 b	a and b are evaluated on the same sampled clock
a ##1 b	b is evaluated on the next sampled clock
a ##5 b	b is evaluated five sampled clocks after a
a ##[1:3] b	b may match one, two, or three sampled clocks after a

A sequence matches only when every required expression is true at its required sampled clock. If one expression is false, that particular sequence attempt does not match.

SVA sequence examples

All four examples use the same small testbench structure. Understanding these repeated blocks first makes each example easier to follow.

module assertion_example creates a self-contained simulation example.

The bit declarations create the clock and signals sampled by the assertion.

always #2 clk = ~clk produces a 4 ns clock period.

The sequence defines the pattern, the property supplies @(posedge clk), and assert property runs the checker.

The initial block drives stimulus; $dumpfile and $dumpvars only save waveforms; $finish stops simulation.

The sequence with timing relationship

It demonstrates how ##5 connects two events across clock cycles. The checker looks for req1 at one positive edge and then looks for req2 exactly five positive edges later.

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 clock toggles every 2 ns, so positive edges occur every 4 ns. The delay ##5 therefore means five positive clock edges, not 5 ns.

Read the checker from inside out: req1 ##5 req2 is the timing pattern; @(posedge clk) selects the sampling edge; assert property(prop) starts an attempt at each positive edge; and the initial block changes req1 and req2 so different attempts can pass or fail.

Relative cycle	Required value and sequence status
0	req1 = 1 starts a possible match
1 to 4	No expression is checked; the attempt remains active
5	req2 = 1 completes the match; otherwise the attempt fails

This property asserts a bare sequence, so a new attempt begins on every positive edge. Whenever req1 is 0 at the starting edge, that attempt fails immediately. Other attempts can remain active for five clocks before failing because req2 is 0 at their completion edge.

For one attempt, req1 = 0 at its starting edge causes an immediate failure. If req1 = 1, the attempt stays active for five more edges. It then passes when req2 = 1 or fails when req2 = 0.

Important timing detail: the testbench sometimes changes a signal at the same simulation time as a positive edge. That can create a race between stimulus and assertion sampling. Follow the relative-clock rule above when analyzing the sequence; reported simulator times can vary when stimulus and sampling occur together.

The sequence with a logical expression

A sequence does not always need a delay. It can contain a normal Boolean expression that checks several signals together on one sampled clock.

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

Because there is no ## operator, the sequence is one clock long. Both signals are sampled on the same positive edge.

The assertion starts at every positive edge. It fails on edges where either signal is 0 and passes on edges where both signals are 1. The $dumpfile and $dumpvars calls only create waveform data; they do not change assertion behavior.

In the stimulus, both signals begin at 0, later become 1 together, and then return to 0 at different times. The assertion therefore demonstrates both matching edges and non-matching edges without any multi-cycle delay.

The sequence with a formal argument

A formal argument lets one sequence definition receive a signal when it is used. Here, the sequence receives en, so the same sequence pattern could later be reused with a different enable signal.

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

The name en appears as a formal argument in the sequence and property declarations. The module signal en is the actual value passed into the assertion instance.

Item	Role
sequence seq(en)	Declares a reusable sequence with one formal argument
property prop(en)	Passes that formal argument into seq(en)
prop(en)	Connects the module signal en to the property’s argument
(req1 \| req2) & en	Matches when at least one request bit is 1 and enable is 1

Before en becomes 1, the complete expression evaluates to 0 even when a request is active. After en becomes 1, either req1 or req2 can make the sequence match.

The expression matches only when en = 1 and at least one of req1 or req2 is 1. If en = 0, enable blocks the match even when a request is active. If en = 1 but both requests are 0, there is still no match.

Follow the argument path from outside to inside: prop(en) passes the module signal into the property; the property calls seq(en); the sequence finally uses that value in (req1 | req2) & en.

Multiple sequences example

Larger rules can be built by joining smaller named sequences. seqA describes a five-cycle timing pattern, while seqB describes a same-cycle logical condition.

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

This example combines two named sequences with overlapping implication |->. Only a successful completion of seqA creates an obligation to match seqB.

Stage	Requirement
Start of seqA	req1 must be true
Five clocks later	req2 must be true, completing seqA
Same completion clock	seqB also requires req1 and req2 to be true

Because the operator is |->, seqB is checked on the same clock where seqA completes. The pass action prints assertion passed; the else action reports assertion failed. If seqA does not match, no consequent check is required for that attempt, which is a vacuous pass.

If seqA never completes, seqB is not required for that attempt. When seqA does complete, both req1 and req2 must be true on the same completion edge; otherwise the consequent fails.

Read seqA |-> seqB as: whenever the complete seqA pattern is observed, seqB must also be true at the exact clock where seqA finishes.

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.

Expression	Meaning
req[*0]	Repeat req zero times; no positive-length occurrence is required
req[*1]	Require req for one sampled clock
req[*0:2]	Allow zero, one, or two consecutive occurrences of req

Empty matches matter when zero is included in a repetition range. They can change the start or end point of a larger sequence, so expand the possibilities when debugging a complicated expression.

Simplify below event sequence

Repetition operators make long timing patterns easier to read and maintain.

Example 1:

Sequence

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

Sequence Simplification

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

Part	Explanation
(req1 ##3 req2)	One request-to-response pattern
[*3]	Repeat that complete pattern three consecutive times
Boundary between repetitions	The next repetition starts on the clock after the previous one ends

Example 2:

Sequence

req1[*0:2] ##1 req2

Sequence Simplification

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

Allowed repetition count	Equivalent possibility
0	req2
1	req1 ##1 req2
2	req1 ##1 req1 ##1 req2

The complete sequence matches if any one of these legal possibilities matches. This is why repetition ranges can create multiple parallel sequence attempts.

Common Mistakes

Treating ##5 as five nanoseconds. It means five ticks of the sequence’s resolved clock.
Asserting a bare sequence when the check should start only after a trigger. Use implication for request-response rules.
Using a level such as req1 when only a new request should trigger the check. $rose(req1) avoids starting another attempt every high cycle.
Confusing |-> and |=>. Overlapping implication starts the consequent on the antecedent’s completion clock; non-overlapping implication starts it on the next clock.
Mixing bitwise & or | with logical intent, especially when operands are wider than one bit.
Forgetting that a repetition range can create several possible matches at the same time.
Reading a pass caused by a false antecedent as proof that the response behavior was exercised. That pass is vacuous.