Assertion Based Verification

By Ashok Kulkarni, Sr. Technical Marketing Manager and Sanjana Nair, Engineering Director of Corporate Applications, Synplicity, Inc.

Imagine a swarm of bees flying about a huge 16th century closed castle. And your mission, sitting blind-folded at a corner chair, is to destroy each bee with a laser gun that can hit one bee at a time. You have two challenges here: poor observability (eyes closed) and poor controllability (away from the target). Traditional verification techniques (simulation, acceleration, emulation) suffer from similar problems because they use a black box approach which involves applying stimuli to inputs and comparing the output results with expected values. Sometimes a bug may be hidden deep inside a design and manifests only after applying several hundred million test vectors and in other cases it may need a special set of vectors that sensitizes the circuit for the bug to be visible. Now imagine the bees are confined to a small enclosure, thousand times smaller than the castle, your eyes wide open and once again you are on the same mission! The new scenario significantly improves the observability and controllability of the target. Assertion Based Verification (ABV) is all about localizing (where it happens) and detecting (when it happens) the bug. Designs that involve third party IP, complex bus interfaces, processors, memories, custom logic and multiple clocks have made verification extremely challenging. Design trends have kept pace with Moore’s law but the verification challenges have grown by an order of magnitude. Finding that last bug takes a significant amount of time which mandates applying new verification techniques.

What are Assertions?

Assertions are explicit expressions of design intent, capturing both the intended and unintended behavior of the circuit structure. By embedding assertions in a design and by having them monitor the design activities, assertions improve observability. ABV creates any desired number of internal test points throughout the design and speeds up debugging by identifying errors close to the source. Assertions also identify problems or circuit behavior that does not propagate to primary outputs exposing bugs that otherwise would go undetected and increasing observability. Assertions can be used in a dynamic environment (e.g. simulator or a design running in hardware with live stimuli) or in a static environment (e.g. formal verification).

Figure 1. Embedding Assertions in a Design

ABV – using Language or Libraries

You may write customized assertions using assertion languages such as Property Specification Language (PSL) or SystemVerilog Assertions (SVA). Alternately, you may use a standard library of pre-defined assertions such as Accellera’s Open Verification Library (OVL). Assertion checkers are composed of one or more properties, a message, a severity, and coverage. In this article we will focus on library based ABV. The OVL is composed of 33 pre-defined assertion checkers that verify specific properties of a design, as well as capture coverage metrics. By using a single, well-defined interface, OVL provides designers, IP integrators, and verification engineers an open, vendor- independent interface for functional verification using static and dynamic verification. The OVL has multiple implementations and the pre-defined checkers are written in Verilog-95, SystemVerilog, and PSL (VHDL expected in the near term) with readily available source code. OVL supports user specific error messaging with several levels of severity. OVL checkers are instances of modules whose purpose in the design is to ensure that the design intent (specification) matches the design behavior (implementation).

OVL Assertion Example

Consider the following verification of a request acknowledgement. For a design to function correctly, after a request condition (bus_req) is asserted, an acknowledge (ack) must occur after 3 and before 6 clock cycles have occurred. In this example only the property of the assertion is discussed. The Verilog example in the diagram is given using the OVL assert_frame module, using the defaults for reporting:

assert_frame # (severity_level, min, max) inst (clk, start_event, check_expr)

assert_frame #(0,3,6) req_ack (clk, bus_req, ack)

Figure 2. OVL Example assert_frame

If ack is not active within 3 to 6 clocks assertion gets triggered when thus indicating that the design implementation is incorrect and fails to follow the specification. OVL provides a variety of checkers based on the design condition or number of cycles involved.

Summary

The benefits of ABV can be summarized by noting that the methodology:

• Provides internal test points in the design
• Accelerates the diagnosis and detection of bugs by localizing the occurrence of a suspected bug to an assertion monitor, which is then checked
• Increases observability and controllability of the bugs
• Uniform reporting structure - Assertion in libraries such as the OVL enable a standard format of reporting errors, warnings and notes. This is particularly advantageous in projects which spread across teams and engineers.
• Intellectual property (IP) providers can provide a set of assertions for each of their designs which can be re-used by the designer to verify the IP when plugged into their design. This alleviates the quality concerns of the designers.
• Unification of the verification process: ABV benefits both the IP provider as well as the end designer by unifying the verification process with a single set of constructs or library models which can be used across all tools including formal verification, simulation, and hardware based verification by synthesizing assertions.

While high capacity and complex FPGA/ASICs have given designers an opportunity to develop system-on-a-chip (SoC) designs the verification of these designs has grown multi-fold. Applying billions of vectors to the input of the design alone will not uncover all the bugs, especially corner case bugs, hidden deep inside. Sometimes the stimuli may not sensitize the circuit for the bug to be visible or in other cases the effects of a bug may not propagate to an observable point. What you need is a White Box approach where the bugs are detected close to the source of the occurrence and flagged right when they occur. This dramatically increases the quality of verification, reduces development costs by discovering bugs that would otherwise go undetected until after silicon fabrication.