Introduction to System Verilog Assertions

In this article we will learn about the assertions and need for it. Before System Verilog assertions were present as part of the HVL. System Verilog introduced various assertions constraint in-built to the HDL. This helped writing complex assertions easily in System Verilog and brough uniformity in assertion constructs. Let us explore the basics of assertions in this article and slowly we will investigate more advanced assertion constructs in future articles.

Introduction

Need for Assertions

In verification, we write various checkers to check the functionality of the design. Basically, in these checkers we will check whether the output from the design matches the expected output for a certain set of input. But with this, we are only verifying functionality and not the behavior of the design.

For example, a spec mentions that output should toggle after 2 clock cycles of the valid input. How will we verify this in our TB? From checker we will only be able to check whether output is correct or not. In these scenarios, assertions are useful, and they help us verify the behavior of the signals. In our example, we can verify whether output signal toggles after 2 clock cycle of valid input or not through assertions.

Advantages of Assertion

Assertions have several advantages over other verification methods, such as:

Assertion helps capture improper behavior of the design near the source of the problem. This reduces the debug time as we root cause assertion issues faster.
For assertion failure, we know the signal involved in one assertion construct. Thus, our debug can be limited to these signals.
Assertions can also be used as functional coverage. This helps us cover some of the behavioral properties which could be hard to be covered in traditional coverage construct.
Assertions can also be used in Formal verification, which is an entirely separate way of verification. Formal verification is different from functional verification and mainly based on assertions.

Different Assertion Languages

Assertion can be implemented in many languages. In Verilog, there is no assertion construct present natively in the Verilog language. Thus, initially there were various languages used for assertion. In System Verilog native support for assertions was added.

Below are some of assertion languages for reference:

PSL (Property Specification Language) – based on IBM Sugar
Synopsys OVA (Open Vera Assertions) and OVL (Open Vera Library)
Assertions in Specman
0-In (0–In Assertions)
SystemC Verification (SCV)
SVA (System Verilog Assertions)

Our discussion will mainly be based on SVA (System Verilog Assertions).

System Verilog Assertions

Prior to System Verilog, different assertion languages were used due to which there were no uniformity in the assertion constructs. There was a need to natively support assertions in HDL itself due to the increasing complexity of the verification.

Advantages of System Verilog Assertion (SVA)

Some of the benefits of SVA are:

System Verilog merges benefits from different assertion languages into one, thus giving the best from all languages.
Due to native support of assertions in SV, assertions can be added to the design and testbench directly without needing to add special interface.
SVA is easy to learn and implement.
Same assertions can be re-used in both functional and formal assertions.

System Verilog supports two types of assertions: immediate assertions and concurrent assertions.

Immediate Assertions

An immediate assertion is a type of instruction that tells a simulator how to check the correctness of a design under test (DUT). It follows the simulation event semantics, which means it will be evaluated in the event regions based on how assertion is used. It is written as a procedural statement, and it is executed like any other statement in a procedural block.

Simply, we can understand immediate assertion as a basic statement which is evaluated for a single time.

Syntax: assert (expression) pass_statement [else fail_statement] .

The expression is non-temporal, and it is treated as a condition in an if statement.
The pass_statement is executed if the expression is true, and the fail_statement is executed if the expression is false.
The else block is optional, but it can be used to specify the severity level of the assertion failure.

Concurrent Assertions

Concurrent assertions are evaluated over a period of time, usually spanning multiple clock cycles. Concurrent assertions are sampled in the prepone region of the event semantics to avoid any race condition, but the property is evaluated in the observed region of event semantics.

Expressions used in concurrent assertion are temporal in nature, which means we can specify behavior over time.

There are various layers of concurrent assertion. Let us see the different layers and their use:

Sequence

Sequence is the basic building block of concurrent assertions in SV. A sequence is a series of Boolean expressions that specify the order and timing of events that form a property. A sequence can be written as a simple sequence, which consists of a single expression, or as a complex sequence, which combines multiple expressions with operators.

Property

A property is a logical expression that describes a condition or a sequence of events that should hold true for the design. We can use sequence in a property or even directly use an expression, if the expression is simple.

Assert directives

As we have seen assertion can be used in formal verification as well as coverage, thus there are multiple assert directives provided by SV.

assert: This statement specifies that a given property of the design should always be true in simulation. If the property evaluates to false, the assertion fails, and an error message is generated.
assume: This statement specifies that a given property is an assumption that guides the formal verification tools to generate input stimulus. The assumption is not checked in simulation, but it can be used to constrain random variables or generate cover points.
cover: This statement evaluates a given property for functional coverage. If the property evaluates to true, a cover point is hit, and a coverage report is generated.
restrict: This statement specifies that a given property is a constraint on formal verification computations. The property is ignored by simulators, but it can be used to prune unreachable states or avoid invalid scenarios.

We can use property with any of the assert directive.

Delay operator

Concurrent assertions have temporal expressions, thus we need some way to provide delay in terms of clock for the expression. ## is clock cycle delay operator. The delay provided by this operator is not based on time scale but rather based on the clock which is inferred by the assertion property.

For example - ##1 means delay of one clock cycle

We can also use ##0 which means the expression should be evaluated on the same clock cycle.

Example

always @(posedge clk) begin
    // some logic
    sequence seq1 ();
	    req ##1 ack;
    endsequence

    assert property (req ##1 ack); // check that ack follows req within one clock cycle

    cover property (seq1); //like above assert property but this time will be used for coverage as cover directive is used.
end

This is just a simple example to give an idea of the concurrent assertions. We will discuss these in more detail in future articles.

Conclusion

In this article, we have learned about the basics of System Verilog Assertions (SVA), which are a powerful way to verify the behavior and functionality of a design under test (DUT). We have seen the advantages of SVA over other assertion languages, and how SVA can be used for both simulation and formal verification.
We have also learned about the two types of assertions in SVA: immediate assertions and concurrent assertions. Immediate assertions are evaluated as procedural statements in a single time step, while concurrent assertions are evaluated over a period of time, usually spanning multiple clock cycles. Concurrent assertions are composed of sequences and properties, which can be used with different assert directives to specify the desired verification goals. In the next few articles, we will explore more advanced features and applications of SVA with some real-scenario examples.