|
Richard Stolzman
Verplex Systems
TechOnline
Recent assertion-standardization achievements hold the promise of improving verification efficiency and allowing formal verification to work with simulation. There are tools that support assertion standardization today, with more promised for the future. The article describes what assertion checking is and what it buys a designer, and shows some examples of assertions used in actual designs.
Defining Assertion-Based Verification
The challenge of application specific integrated circuit (ASIC) and system-on-chip (SoC) verification has kept many engineers awake on many a night. With ever-increasing design complexity comes the associated realization that the effort required to verify these designs is increasing at an even faster rate. And, the problem goes further. While designer productivity underwent a breakthrough gate-per-hour increase with the adoption of synthesis, a comparable breakthrough did not happened in verification productivity.
What does this have to do with assertions? First, let's define what an assertion does. In software programming, an assertion is an expression that, if false, indicates an error. Assertions are used for debugging by catching can't happen errors. Within hardware description language (HDL) designs, an assertion is a conditional statement that checks for specific behavior and displays a message if it occurs. Assertions are generally used as monitors looking for bad behavior, but may be used to create an alert for desired behavior as well. For our purposes, an assertion is a statement about a specific functional characteristic or property that is expected to hold for a design.
Assertions have been used in HDL verification for many years. This may seem confusing to some people, since they may have never realized they were using what are now called assertions. They were used in simulation, generally as a backup to other methods. The promise of assertion-based verification goes far beyond this early usage to establish assertions as an enabler of much more efficient verification, simplified analysis, and the synergistic use of simulation and formal verification methods.
An understanding of assertion-based verification is obtained by extending the capabilities of assertions by employing a methodology that utilizes them as a central target for a variety of verification methods. Assertion-based verification is the use of assertions for the efficient verification of a collection of partial specifications by the synergistic application of simulation, formal verification, and semi-formal verification.
A Brief History of Assertions
Designers historically had the ability to craft assertions using both the Verilog and VHDL design languages. Lacking an assertion statement, the Verilog designer used a conditional statement to trigger the output of an error message. The VHDL designer used the assert statement inherent in VHDL to check for the violation of a condition and to output a message.
Generally, assertions were added during verification to monitor conditions that were otherwise hard to check using simulation. And sometimes, they were used to simplify the debugging of complex design problems. Assertion monitors can be thought of as internal software test points that wait for a particular problem to happen and then alert the designer when it does. In these cases, assertions were used to improve observability, which means the ability to observe bugs once they are triggered by a simulation vector. Without assertions, test vectors had to be much longer to ensure that triggered bugs were propagated to observable outputs, else the errors remained undetected. By adding assertions, bad behavior inside the design could be checked and the bugs were observed instantly, at their source.
More recently, assertions are being used successfully with formal verification. The use of assertions as targets for formal verification is used to improve controllability. Low controllability is the problem that occurs when the number of simulation vectors needed to penetrate and thoroughly stimulate the potential functional mistakes buried within a design becomes prohibitive. As a simple example, consider a 32-bit comparator. To test for a worst-case single-bit bug, you need 264 vectors (Figure 1). Using the fastest simulator today, this would take over half a million years to verify. By performing the formal verification of an assertion, the same verification is completed in less than a minute. The important point is that due to design complexity it is often impossible to create a minimal set of sequential patterns that adequately sensitize a design in the correct way, and control all of the sequential elements needed to trigger errors using simulation.
By using assertions as properties, the controllability problem is reduced or eliminated by adding and formally verifying those assertions in the design. As a result, the formal verification of assertions yields significant advantages in both observability and controllability.
Figure 1: Even with a one-million cycle-per-second simulator, checking for all possible single-bug errors in a 32-bit comparator would take almost 600,000 years
Summarizing, assertion-based verification benefits users by:
- Providing internal test points in the design
- Simplifying the diagnosis and detection of bugs by localizing the occurrence of a suspected bug to an assertion monitor, which is then checked
- Allowing designers to verify the same assertions using both simulation and formal verification
- Increasing observability when simulation is used
- Increasing both controllability and the observability when formal verification is used.
A Revolution in Verification
The revolution began with the idea of methodically using assertions to create implementation-level behavioral checks in register transfer level (RTL) designs. Designers, as they created an RTL implementation with the desired behavior, included assertions to make sure the behavior could be verified directly. This created some extra work on their part, but compensated by greatly reducing verification and debug effort.
In addition, since the assertions were included in the design as it was created, formal verification could be started earlier, before any test vectors had been written. Assertions were also used at the design boundaries to provide checks for interface behavior. This was useful as design modules from different designers are integrated. Such interface-checking assertions made modules more portable; they preserved the intimate design knowledge needed to verify them as part of a larger system. As a result, modules with embedded assertions became self-checking wherever they were later reused. The net benefits resulted in finding problems sooner, spending less time analyzing them, reaching a stable design verification point sooner, and simplifying integration and design reuse.
The next part of the revolution came with the efforts of the Open Verification Library initiative. This began with the realization that a standard method of defining more complex assertions was needed. A method was needed that could be used and understood by designers in different groups, at different sites, and at different companies. Furthermore, a consistent specification mechanism was needed for both simulation and formal tools without the need for proprietary languages. The Open Verification Library (OVL) started as a donation by Verplex Systems of an assertion library for open source standardization. Today, OVL is the only existing assertion-specification standard in Accellera that currently works with any IEEE-1364 (Verilog) and IEEE-1076 (VHDL) compliant simulator. It also works with a growing number of formal-verification tools (Figure 2).
Figure 2: Using assertions accelerates design development by improving debug observability and controllability
Anatomy of an Assertion
In the past few years, the verification community has seen the emergence of a plethora of proprietary assertion languages and unique assertion interfaces for the various design verification tools. Most of these languages and interfaces are not native to the designer's verification flows, requiring designers to master new verification techniques and interfaces. In short, many of these assertion methods were developed for exclusive use with one tool, necessitating extra work to re-write assertions in different formats when the use of multiple verification tools was desired.
In its simplest form, an assertion consists of the function to be monitored. This assertion can be easily implemented in Verilog or VHDL by the designer, which often raises the question of why any special assertion language or method is needed at all. The answer becomes clear when the designer extends the creation of assertions to include common modes of usage, operation and reporting. The ideal of assertion-based verification goes beyond function capability to include usability and methodology.
As an example, consider a simple assertion to verify that a certain logical condition cannot happen. In OVL, this is performed by assert_never. While a designer could create an assertion to check for this condition in a few lines of Verilog or VHDL code, the OVL library module for assert_never is over a page in length. In addition to the functional check itself, OVL assertions are structured so they will not affect design behavior or synthesis results. Additional mechanisms are provided so the assertions can be disabled, a level of severity for the error can be easily specified or the number of failures counted. It quickly becomes apparent that a well-conceived and well-defined library of assertions has notable benefit. By selecting an assertion from a library, a standardized set of functionality and user options is provided.
As another example, consider the following verification of a request acknowledgement. For a design to function correctly, after a request condition (req) is asserted, an acknowledge must occur after 3 and before 7 clock cycles have occurred. The Verilog example in the diagram is given using the OVL assert_frame module, using the defaults for reporting (Figure 3).
Figure 3: This Open Verification Library (OVL) example shows the verification of a request acknowledgement in Verilog
Looking Ahead
Accellera currently has three standardization efforts underway that will further enable assertion-based verification:
- Formal Property Language—Sugar
- SystemVerilog Assertions
- Open Verification Library (OVL).
First, there is a formal-property-language effort, which is defining the Sugar language standard for property specification. This will provide new capability to express abstract, higher-level specifications of design functionality. Next there is the effort to add a native assertion construct and capability to SystemVerilog. This will provide a simpler and more expressive way of including assertions directly in Verilog designs. Finally, the OVL effort defines the standard library of assertions, providing a consistent method of reporting and controlling these assertions.
Individually, the three efforts are synergistic by providing a new property-specification language, new assertion capability in Verilog, and an HDL, language-independent library of pre-packaged and pre-verified assertions. Together, they enable assertion-based verification to occur at various levels throughout the design flow, suiting the needs of the block-level designer, the system-level integrator, and the design architect.
Summary
Assertion-based verification directly addresses the limitations of today's verification flows. It increases observability in simulation while providing targets for formal verification, which increases controllability. Furthermore, assertions facilitate design reuse through self-checking code.
In assertion-based verification, RTL assertions are used to capture design intent in a verifiable form as the design is created, providing portable monitors that check for correct behavior. During simulation, assertions improve observability coverage, making the source of an error evident. Simulation debug time is greatly reduced. As targets for formal verification, assertions improve controllability coverage. When verifying assertions, formal verification algorithms explore the equivalent of billions and billions of input patterns without requiring test vector creation. And ideally, the same assertions are used for both simulation and formal verification so there is no need to repeatedly specify the same assertions multiplied different ways for different tools.
Assertion-based verification is a multi-faceted approach to verifying a collection of partial specifications more efficiently. Assertions enable capabilities for both simulation and formal verification and, in the case of open standard assertions, a common method of capturing intimate design knowledge for both.
|
