Verification with assertions refers to the use of an assertion language to specify expected behavior in a design, and of tools that evaluate the assertions relative to the design under verification.

Assertion-based verification is mostly useful to design and verification engineers who are responsible for the RTL design of digital blocks and systems. ABV lets design engineers capture verification information during design. It also enables internal state, datapath, and error precondition coverage analysis.

Simple example of assertion could be a FIFO: whenever a FIFO is full and a write happens, it is illegal. So a FIFO designer can write an assertion which checks for this condition and asserts failure.

Currently there are multiple ways available for writing assertions as shown below.

• Open Verification Library (OVL).
• Formal Property Language Sugar
• SystemVerilog Assertions

Most assertions can be written in HDL, but HDL assertions can be lengthy and complicated. This defeats the purpose of assertions, which is to ensure the correctness of the design. Lengthy, complex HDL assertions can be hard to create and subject to bugs themselves.

In this tutorial we will be seeing verilog based assertion (OVL) and PSL (sugar).

• Testing internal points of the design, thus increasing observability of the design.
• Simplifying the diagnosis and detection of bugs by constraining the occurrence of a bug to the assertion monitor being checked.
• Allowing designers to use the same assertions for both simulation and formal verification.

Assertion monitors address design verification concerns and can be used as follows to increase design confidence.

• Combine assertion monitors to increase the coverage of the design (for example, in interface circuits and corner cases).
• Include assertion monitors when a module has an external interface. In this case, assumptions on the correct input and output behavior should be guarded and verified.
• Include assertion monitors when interfacing with third party modules, since the designer may not be familiar with the module description (as in the case of IP cores), or may not completely understand the module. In these cases, guarding the module with assertion monitors may prevent incorrect use of the module.

Normally assertions are implemented by the designers to safeguard their design, so they code the assertions into their RTL. A simple example of an assertion would be: writing into FIFO, when it is full. Traditionally verification engineers have been using assertions in their verification environments without knowing that they are assertions. For verification a simple application of assertions would be checking protocols. Example: expecting the grant of an arbiter to be asserted after one clock cycle and before two cycles after the assertion of request.

In the next few pages we will see simple examples on usage of assertions using Open Verification Library and PSL assertions.

For using Open Verification Library examples you need Open Verification Library from Accellera. For running PSL examples you need a simulator that can support PSL.

Then you need a bit of patience to go through the manuals to learn in details Assertions and try out more examples.

Copyright © 1998-2014

Deepak Kumar Tala - All rights reserved

Do you have any Comment? mail me at:deepak@asic-world.com