System Verilog Assertion Constructs (1)

11 Nov 2023

6 mins

In previous article we discussed about assertions in general and also looked into the basics of System Verilog Assertions, commonly known as SVA. SVA brought lots of good features from different assertion languages into one and thus it is the most used assertion language nowadays. In this article we will explore deeper into concurrent assertions of SVA and learn different constructs provided by SVA which helps write complex assertion.

Sequence in detail

In SVA, sequences are the basic building blocks of a concurrent assertion. A sequence is a series of Boolean expressions that specify the order and timing of events that form a property.

As concurrent assertions are time dependent, thus there should be a clock associated with all the sequence. If a clock is not explicitly mentioned in the sequence body, then the clock of the parent property is implied and used for the sequence.

Syntax:

sequence <seq_name>
    <event clock>
	[Boolean expression]
endsequence

Delay operator

In concurrent assertions, we check the behavior of the signals spread across time periods. Which means that expressions are temporal in nature, and we need to provide delay in terms of clock. SVA provides ## operator also known as delay operator to provide delay.

##0 -> means that there should be no delay and expression on LHS and RHS should hold true at same time.

##1 -> means that the expression present on RHS should be true after one clock cycle of LHS.

We can also provide a range in the delay. This is useful when there can be some unknown clock delays. Consider an example of ALU which asserts valid signal 2-4 clock cycles after the input has been given. We can use delay operator as follow:

input_data ##[2:4] valid -> assert statement will fail if valid is not set to 1 within 2 to 4 clock cycles after input_data becomes 1.

Repetition operator

Repetition operators are used when a certain expression or sequence repeats itself for a certain period.

In our previous ALU example, let us suppose the valid signal should be asserted for two cycles. A possible assertion for this scenario would be input_data ##[2:4] valid ##1 valid. Using repetition operator this can be simplified and rewritten as input_data ##[2:4] valid [*2]

Repetition operator is of three types:

• Consecutive repetition operator [*<repition_val>]
• Non-consecutive repetition operator [=<repition_val>]
• Go-to repetition operator [-><repition_val>] Where repetition_val can be a number or range

Consecutive repetition operator

This operator indicates that the expression or sequence repeats itself specified number of times consecutively.
Example - s1 ##3 s2 [*3] is equivalent to s1 ##3 s2 ##1 s2 ##1 s2

Like delay operator we can provide a range of values to the repetition operator as well.
Example - s1 ##3 s2[*2:3] is equivalent to s1 ##3 s2 ##1 s2 or s1 ##3 s2 ##1 s2 ##1 s2. Assertion will pass if s2 is asserted for 2 or 3 clock cycles.

Non-consecutive repetition operator

Non-consecutive repetition indicates that the expression or sequence repeats itself specified number of times, but the occurrence may or may not be consecutive.

Example - s1 ##2 s2 [=3] ##4 s3 here Boolean expression s2 has been true thrice, but not necessarily on successive clocks. The first occurrence of s2 happens after two clocks cycles of s1. The last occurrence of s2 is at least four clock cycles before s3.

Goto repetition operator

Goto repetition operator is like non-consecutive repetition operator except that in goto repetition operator penultimate occurrence should be true.

Example - s1 ##2 s2 [=3] ##4 s3 here Boolean expression s2 has been true thrice, but not necessarily on successive clocks. The first occurrence of s2 happens after two clocks cycles of s1. The last occurrence of s2 should exactly be four clock cycles before s3.

System functions in SV useful in assertions

System Verilog provides different system functions which makes writing assertions easier. Let’s see some of these functions and their use.

$rose

This function returns one if the LSB of the expression changed to 1. Basically, this detects positive edge of a signal like @posedge. Though functionality is similar, $rose cannot be interchanged with posedge.

posedge is not a function but an event and thus cannot be called everywhere. On other hand $rose is a function which return 1 when it detects positive edge.

$fall

This function returns one if the LSB of the expression changes to 0. This means that $fall detects negedge of a signal.

$stable

This function will return one if the value of the signal does not change over time, i.e., if signal remains stable.

$past

This function takes 2 args as input, expression_name and no_of_cycles and returns the sampled value of the expression which was present no_of_cycles prior to the time of calling this function.

Example 1: req-ack checker

Design statement - The ack from the design should follow the req within 5 cycles. Also, the ack should stay high for 4 cycles continuously.

We will see how to write assertion for above behaviour using delay and repetition operator.

module test();
    reg ack, req;
    bit clk;

    sequence sq1;
        @(posedge clk) // event clock defined inside sequence
        $rose(req) ##[1:5] ack [*4];
    endsequence

    assert property (sq1)
        $info("sq1 assert PASSED"); // optional - pass message
    else
        $warning("sequence sq1 assertion FAILED"); // optional - failure severity set to warning

    always begin
        #10 clk = ~clk;
    end

    // Test sequence
    initial begin
        // Passing scenario
        #20;
        @(posedge clk) req <= 1;
        #1;
        @(posedge clk) ack <= 1;
        #1;
        repeat(4) @(posedge clk);
        req <= 0;
        ack <= 0;

        // Failing scenario
        #20;
        @(posedge clk) req <= 1;
        #1;
        @(posedge clk) ack <= 1;
        #1;
        @(posedge clk) ack <= 0; req <= 0;

        // Failing scenario
        #20;
        @(posedge clk) req <= 1;
        #1;
        repeat (6) @(posedge clk);
        ack <= 1;
        #1;
        repeat(4) @(posedge clk); req <= 0; ack <= 0;
    end
endmodule

Output

# ** Warning: sequence sq1 assertion FAILED
#    Time: 10 ns Started: 10 ns  Scope: test File: assertions_delay_1.sv Line: 12
# ** Warning: sequence sq1 assertion FAILED
#    Time: 30 ns Started: 30 ns  Scope: test File: assertions_delay_1.sv Line: 12
...
# ** Info: sq1 assert PASSED
#    Time: 130 ns Started: 50 ns  Scope: test File: assertions_delay_1.sv Line: 11
...
# ** Warning: sequence sq1 assertion FAILED
#    Time: 270 ns Started: 170 ns  Scope: test File: assertions_delay_1.sv Line: 12
...
# ** Warning: sequence sq1 assertion FAILED
#    Time: 330 ns Started: 230 ns  Scope: test File: assertions_delay_1.sv Line: 12

In above output we can see that assertion is evaluated in each posedge of the clock and if any of the expression fails our assertion fail. Therefore, in clk edge where $rose(req) is false is also considered as failing condition. These failures are not correct as our assertion is valid when req is asserted and so the assertion should start checking only when we $rose(req) is true. This is achieved using implication operator which we will see later.

Example 2: reset checker

Design statement – The reset should be asserted at least thrice during the power-on sequence, i.e., when power_off signal goes lows. Also reset done should be toggles after 2 clock cycles of the 3rd reset assertion

We will implement two assertions for the above statement one with goto repetition operator and another with non-consecutive repetition operator and see the different between them.

module test();
    reg power_off, reset, reset_done;
    bit clk;

    sequence sq1; // sequence with non-consecutive repeatition operator
        $fell(power_off) ##1 reset [=3] ##2 reset_done;
    endsequence

    sequence sq2; // sequence with goto repratition operator
        $fell(power_off) ##1 reset [->3] ##2 reset_done;
    endsequence

    assert property (@(posedge clk) sq1)
        $info("sq1 assert PASSED");
    else
        $warning("sequence sq1 assertion FAILED");

    assert property  (@(posedge clk) sq2)
        $info("sq2 assert PASSED");
    else
        $warning("sequence sq2 assertion FAILED");

    always #10 clk = ~clk;

    initial begin
        #10;
        // passing sequence for sq1
        @(posedge clk) power_off <= 0; reset_done <= 0;
        #1;
        repeat(3) begin
            @(posedge clk) reset <= 1;
            #1;
            @(posedge clk) reset <= 0;
            #1;
        end
        // reset_done is asserted 5 clocks after reset is 1.
        repeat(4) @(posedge clk); reset_done <= 1;
        #10;
        @(posedge clk); reset_done <= 0; power_off <= 1;

        #10;
        // passing sequence for both sq1 and sq2
        @(posedge clk) power_off <= 0;
        #1;
        repeat(3) begin
            @(posedge clk) reset <= 1;
            #1;
            @(posedge clk) reset <= 0;
            #1;
        end
        // reset_done is asserted 2 clocks after reset is 1.
        @(posedge clk); reset_done <= 1;
    end
endmodule

Output

# ** Warning: sequence sq2 assertion FAILED
#    Time: 10 ns Started: 10 ns  Scope: test File: assertion_repeatition.sv Line: 21
...
# ** Info: sq1 assert PASSED
#    Time: 250 ns Started: 50 ns  Scope: test File: assertion_repeatition.sv Line: 14
...
# ** Info: sq2 assert PASSED
#    Time: 430 ns Started: 290 ns  Scope: test File: assertion_repeatition.sv Line: 19
# ** Warning: sequence sq1 assertion FAILED
#    Time: 430 ns Started: 430 ns  Scope: test File: assertion_repeatition.sv Line: 16
# ** Info: sq1 assert PASSED
#    Time: 430 ns Started: 290 ns  Scope: test File: assertion_repeatition.sv Line: 14

In the above output we see that for the first test sequence only sq1 passes as the reset_done comes 5 clock cycles after reset is asserted for 3rd reset time. For goto operator to pass the reset_done should come exactly 2 cycles after reset is asserted for 3rd time. Thus, in 2nd test sequence we see that both sq1 & sq2 passes.

Wave

Conclusion

In this article, we have learned about the different constructs and functions that System Verilog Assertions (SVA) provides to write complex and temporal properties. We have seen how to use delay, repetition, and system functions to specify the order and timing of events in a sequence. We have also seen some examples of how to use these constructs to check the behaviour of a design under test. SVA is a powerful and expressive language that can help us verify the functionality and performance of our hardware designs. In next article we will explore some more advanced topic of SVA.