Assertion-based verification

What is assertion-based verification?

Assertion-based verification (ABV) is a technique that aims to speed one of the most rapidly expanding parts of the design flow. It can also be used in simulation, emulation and silicon debug.

Research has suggested that verification can take up 70% of the time and cost of a full design cycle and that, within that, functional verification can take up more than half of the verification time. A number of studies have concluded the use of ABV reduces functional verification dramatically compared with traditional methods. One of the most widely cited studies is from a 2000 paper presented at the 12th International Conference on Computer Aided Verification by IBM Research in Haifa, Israel, which claimed a 50% reduction in verification effort through the use of the same formally derived assertions during the unit, subsystem and system verification phases.

However, a distinction must be drawn between the use of assertions and their integration within a coherent and effectively implemented methodology. To understand this, we first need to consider assertions in isolation and the challenge they present.

What are assertions?

One way of considering assertions is to say that they are active comments. Where design and verification engineers have historically inserted passive code into a design to describe the intent of what is being exercised at a particular point in RTL or testbench code, assertions are “executable specifications”.

They describe either legal or illegal behavior that can be observed at the point of their insertion by tools, and then flagged as having passed or failed. In itself, this is an easy-to-grasp extension of  how comments work (and indeed passive comments are still added to assertions to ease communication as to their purpose between various participants in a design project). They are well suited to control signals because they are inherently specific.

In addition to their specification aspect, assertions should also include some coverage properties to help ensure thoroughness of the verification and later aid in the gathering of metrics that help to assess not only their benefit on an individual project but also how well the technique is being generally implemented.

Assertions are essentially produced in three forms.

• The design engineer will insert them in the main design file alongside the code to be verified.
• The verification engineer  will insert them in the bind files used as part of the verification process.
• A third party – a standards group or a tools vendor – will provide a library of off-the-shelf assertions for common use-cases.

The most commonly used non-proprietary library is the Open Verification Library (OVL), originally developed by Accellera (now the Accellera Systems Initiative).

Assertions are today main written in two languages (although historically a wider range has been used).

• SystemVerilog Assertions (SVA) is a subset of the SystemVerilog (IEEE 1800) combined hardware description and verification language, and is now by far the most popular format.
• The Property Specification Language (PSL) (IEEE 1850) is predominantly used by engineers working in VHDL environments, but also has variants for SystemC, Verilog and SystemVerilog.

There are then two types of assertion.

• Concurrent assertions must always be satisfied by a design.
• Temporal assertions must by satisfied by the design under certain defined (often clock-based) conditions. These conditions can either contain an individual set or a sequence of sets.

What are the benefits of assertions?

The benefits of assertions fall into four broad categories.

1. Reducing verification time

In 2002, Richard Stolzman of Verplex (now part of Cadence Design Systems) calculated that it would take almost 600,000 years for a one million-cycle-per second simulator to check every possible single-bug error in a 32bit comparator. Even allowing for increases in computational power since then, the exclusive use of such formal verification strategies remains unrealistic.

By focusing parts of the verification process on intent rather than every possible configuration, assertions can inherently reduce the overall cycle time massively, when they are properly used and implemented with sufficient coverage.

2. Catching errors earlier

By encouraging designers to include assertions at the block level, they raise the abstraction level of the overall verification process above a point where the designer might consider his or her work on a subsystem to be complete and ready for hand-off to the verification engineer.

Not only design time but also cost can be cut by capturing errors before they require a larger-scale respin of RTL.

3. Focusing the design effort

Designers who have worked with assertions say that the process has forced them to concentrate more closely on realizing a project’s objectives.

Similarly, the early incorporation of assertions within RTL – as opposed to those assertions that verification engineers later develop for testbenches – improves communication between the teams working on different aspects of a design flow. For example, they can prove particularly useful as prompts when verification engineers are drafting plans and testbenches.

4. Pinpointing sources of error

Assertions should be coded closely to those elements in the design that they verify. Then, when they do flag an error, it is easier to trace it back to its source.

What are the challenges with assertions?

Assertions have obvious potential benefits, but the challenges they present are less immediately apparent. In broad terms, these challenges can be split into four categories.

1. Implementation

A major problem during the initial phase of the adoption of assertions was their inconsistent implementation. This was especially the case where designers with a consequently more limited understanding of verification strategies were asked to write them.

Assertions would be inserted at some parts of the RTL, but not others. As much as they can focus a designer on delivering intent, those designers could equally fall prey to real-world pressures (e.g. schedules) that meant their coding was considered a lower priority, or was simply forgotten.

This could also introduce some confusion for verification engineers, with incomplete sets of assertions directing their attention to limited areas of the overall intent. Moreover, even when assertions were inserted, they sometimes lacked appropriate documentation and, more damaging, coverage information.

This problem has declined given that assertions have now been in use for more than two decades, but it has not entirely disappeared.

2. Coding and debug

A certain level of language proficiency is needed for either SVA or PSL to take full advantage of assertions. This is not always available within the design team – at least not on the scale that may be needed for a complex project.

The languages have their own quirks and twists. Many design managers feel they must balance the need to master the technologies against the time that it may take productive engineers with projects in hand to gain that mastery.

Meanwhile, even trained SVA users often say that they find the language difficult to work with, both for coding and debug. Among designers, one consequence of this is that they will tend to write ‘simpler’ (i.e. one/two-cycle assertions) than may be optimal. Verification engineers also complain that composing temporal SVA assertions is especially challenging.

3. Customization

The flexibility of off-the-shelf assertions is arguably an extension of the coding issue, but still merits consideration in its own right.

The OVL provides a set of standard assertions for common use-cases, but the increasing complexity of subsystem and system design has led to ever greater complaints that they lack an ability to be customized to meet rapidly changing design intent requirements.

The same is said of the assertion libraries provided by vendors which, though more regularly  updated, are also engaged in trying to keep up with the design landscape, particularly as consumer devices require ever increasing functionality.

Customization – and the subtleties it therefore requires – again stresses the need for design and verification teams to maintain sufficient local expertise in assertion languages.

4. Metrics

Any assertion process must have a structured way of reporting and tracing errors, a working coverage database, and techniques that allow for thorough ongoing analysis both within and across projects, as well as a tightening of the integration between simulation, emulation and verification.

ABV must not simply do its job but also be seen and acknowledged to have done its job, if the technique is to gain currency within the user company.

Why do I need an assertion-based verification methodology?

In a DAC 2008 Accellera workshop, Harry Foster of Mentor Graphics suggested four questions that companies should ask themselves to assess how well they were balancing the benefits of and challenges with assertions, and whether they were fostering the right strategy for their use:

1. What is required to mature a project team’s ABV skills for successful adoption?
2. What needs to be considered in terms of a project’s ABV infrastructure (beyond commercial tools)?
3. What metrics need to be defined and gathered to measure progress?
4. What benefits are real industry projects seeing using OVL/SVA/PSL?

The leading tool vendors now provide ABV methodology structures within their simulation, verification and emulation software suites.

There have also been a number of useful attempts to produce software that automates the generation of assertions or makes SVA easier to compose by using a graphical environment.

Users can leverage all of these technologies to gain great benefits from assertions and ABV. But even as more and more companies claim to use the technique, there remain many who use assertions on an as you go basis believing they are operating ABV, but still lacking a true methodology. Others have methodologies which could be made more effective.

What else can I do with assertions?

Assertions are often thought of as a technique that is used to get a design right before it is committed to silicon. But if you are prepared to carry the extra manufacturing cost, it’s possible to synthesize assertions into logic gates that get built into the final chip. Careful design of the assertions can improve the controllability and observability of your logic design, making it easier to  find deeply buried bugs during post-silicon validation. There’s more on this topic here.