SVA : Introduction

Introduction

There is a popular statement about assertion, which says “an assertion is a statement that a given property is required to hold and a directive to verification tools to verify that it does hold”. In other words, an assertion specifies a behavior of the system and it is primarily used to validate the behavior of a design. This can also be used to provide functional coverage and generate input stimulus for validation.

Purpose

Main purpose of assertion is to make sure that the design matches with its specification, which means designer really created what he had intended. When you look deep into different assertions you can see that error detection, error correction and error notifications are the main features of assertions.

Assertions - Verification Approaches

Assertions will be checked dynamically or statically depending on the approaches you follow in your verification. It supports following verification approaches.

Simulation

The assertion checks in simulation are dynamic. A simulator must continuously check, if the actual behavior of the design matches with the specified property. If there is no match, it must report an error.

Formal property checking

These types of assertion checks are static. Formal property checker tries to formally prove that the specified property holds under all possible input conditions. If it fails it generates a counterexample that visualizes the erroneous behavior.

Semi-formal approaches:

These types of assertions checks are partly dynamic and partly static. In this approach, the verification tool starts simulating till some specific interested state and then continues with a formal prove in order to overcome complexity issues.

Classes of Assertions

Immediate Assertions:

Immediate assertions follow simulation event semantics for their execution and are executed like procedural statements. These are very similar to the VHDL assert construct and are used to check specified condition at a certain point of time. Immediate assertion expressions are non-temporal and boolean and is interpreted the same way as an expression in the condition of a procedural if statement. When simulation proceeds to the assertion statement, the condition is evaluated and upon the result of this evaluation the corresponding action is executed. Therefore, immediate assertions are allowed in a sequential surrounding like initial and always blocks, tasks, and functions etc.

statement ::= [ block_identifier : ] statement_item statement_item ::= ... | procedural_assertion_statement procedural_assertion_statement ::= concurrent_assertion_statement | immediate_assertion_statement immediate_assertion_statement ::= simple_immediate_assertion_statement | deferred_immediate_assertion_statement

procedural_assertion_statement ::= ... | immediate_assert_statement immediate_assert_statement ::= assert ( expression ) action_block action_block ::= statement _or_null | [ statement ] else statement

An example of immediate assertion is shown below.

time t; always @(posedge clk) if (state == REQ) assert (req1 || req2); else begin t = $time; #5 $error("assert failed at time %0t",t); end

The action block can be associated with every assertion. An action block specifies actions that are to be executed if the assertion passes or fails. These actions are called as pass or fail statement. For an assertion all combinations of actions can be specified like pass, fail, both or none.

Concurrent Assertions

Concurrent assertions are based on clock semantics and are evaluated continuously with every clock edge. Concurrent assertions can be temporal that means usually it describes a certain behavior that spans over a time interval. More detailed explanation about concurrent assertions can be found in the concurrent assertion section.

Location of Assertions

Inline Assertions

If SVAs are placed directly into System Verilog or Verilog design code or placed as pseudo comments (similar to PSL) into VHDL design code, it is called inline assertions.

Instantiated Assertions

If module containing SVA is instantiated into a VHDL architecture or a System Verilog or a Verilog module, it is called instantiated assertions.

Bound Assertions

It is possible to bind RTL (VHDL or Verilog) and System Verilog module using System Verilog bind-statement. This type of assertions is called bound assertions. This helps to leave the design code untouched or unchanged.

Verification directives

A property itself is completely passive and is never evaluated on its own. The verification directive states the action to be taken for an instantiated property. System Verilog has five different verification directives assume, assert, cover, restrict and expect to state the actions. Assert, cover, assume, and restrict are assertion statements, while expect is a blocking procedural statement.**- Assume:This specifies the property as an assumptions for the environment, i.e. assumes that a property holds.- Assert:This specifies the property as a checker, that means it verifies that a property must hold.- Cover:This monitors and counts expected behavior, in other words monitors the property evaluation for coverage.- Restrict:This specifies the property as an constraint for Formal Verification- Expect:**This waits blocking until a property holds or fails