Assertion-Based Emulation Methodology

by Steven Wang, Axis Systems
Sunnyvale, California USA

Abstract :
Many people are predicting that assertions will be the next big breakthrough to enable engineers to continue to design and verify larger and more complex designs. Assertion-based methodologies bring much-needed structure to the current set of ad-hoc testbench and monitoring techniques used by most projects for simulation, as well as enable more widespread adoption of emerging formal and semi-formal verification technologies.

In this paper, Axis will discuss the new terms and definitions associated with assertions, as well as the proposed multiple methodologies. The discussion will cover terms, such as Assertion, Property, Constraint, Event, Procedural Assertion, Declarative Assertion, and Formal Property Language. The paper will further explore a number of assertion methodologies, such as Open Verification Library (OVL), SystemVerilog, Open Vera Assertions (OVA), Sugar, and 0-In CheckerWare, and explain how to determine which method is best for a specific condition. One of the advantages of assertion-based methodology is its application in an emulation environment. Emulation has long suffered from poor visibility and the move to assertions greatly improves emulation debug. This paper will also discuss an interrupt-driven event-based emulation technology that enables access to behavioral code, such as $display or PLI, as assertion failures are detected in emulation.

The Verification Challenge
As today's designs push past 1M gates and move toward 10M gates, engineers require new tools and methodologies to verify these devices. Unfortunately, some engineers expect to verify these chips using the same waveform dumps, adhoc testbench code with $display statements, and scripts with log file greps to monitor simulation results.

What is needed is a common methodology that will propel the use of assertions across a wide variety of tools ranging from formal verification to logic simulation to emulation. This common methodology will provide increased automation and enable the full benefit of the write-once characteristic of assertions.

Axis is participating in making this vision a reality by educating engineers on the value of assertionbased verification and making sure assertion-based methodologies work well with its simulation, simulation acceleration, and emulation products. The combination of assertions with the generalpurpose ReConfigurable Computing (RCC) verification platform for simulation, simulation acceleration, and emulation will provide users with the needed performance and debugging to meet verification requirements for the next generation of designs.

Introduction to Assertions

Assertions document the designer's assumptions and the properties of the design. They are a powerful tool to crosscheck the design's actual versus intended behavior. They are also valuable to verification and system engineers to formally specify the intended behavior of the system and to make sure it is behaving according to specification. Recently, much has been written about assertions, and even though the concept has existed for years, there is still much confusion over assertions. Before getting into the details of how assertions are specified and implemented, it is useful to look at the motivation behind why assertions are so important.

Assertions provide a common format for multiple tools. Without an agreed-on method of specifying assertions, there is no chance to automate activities, such as functional coverage metrics, error reporting, and severity levels. A common assertion methodology lends itself to increased automation in both formal verification and simulation. Assertions can also benefit from a "write-once, run-anywhere" characteristic. Once inserted into a design, they can be used by many tools and are quite portable for design reuse.

Assertions are better than a paper test plan. Verification involves deriving a list of features to be tested from the design specification. Most projects write a test plan that dictates how the features of the design are to be verified. These features are then documented, and a testcase is developed to verify each feature. Testcases usually take the form of a testbench that will cause the desired feature to be exercised. This directed approach is commonly augmented with random testing. Assertions help to automate the manual process of running a testcase: visually verifying the test has covered the feature and adding the test to the regression suite. Without using assertions, there is often no way to guarantee that the testcase still exercises the feature as the design evolves. Assertions provide a mechanism to measure functional coverage and quantify test results.

Assertions ease debugging and reduce simulation time. One of the main motivations for assertions is reduced debugging time. Since assertions are a white-box verification technique, they provide increased visibility and controllability of the design under test. Assertions will detect design errors as soon as they occur without waiting for the effects to be propagated to the device or system boundaries. Having an immediate indication of a problem can save hours of trying to look backward to get to the root cause of the problem. The use of assertions has been reported to reduce debugging time by as much as 50% [1]. Assertions can also save simulation time since they can terminate a simulation when a fatal error occurs. A runaway or meaningless simulation can waste valuable simulation time if it occurs during an overnight regression run when more tests could be given a chance to run.

Assertions verify interfaces between blocks. During integration phases, assertions act as watchdogs at the module or block interface boundaries making sure each block obeys the agreed-on protocol. This can be crucial since it is possible for a testcase to pass, based on the data observed at the chip or system boundaries, even when there is a violation of a protocol inside the design. Assertions help eliminate such situations.

Assertions are a good RTL coding practice. Assertions are far more valuable than comments alone in the design. Well-commented code makes it easier to maintain and to understand the intended functionality. Assertions go one step further by documenting exactly what the code is expected to do in a way that can be verified using tools instead of a person reading the comments and attempting to understand if the code is working correctly. Assertions are also a good way to sanitize the code before check-in. Tools can read a design file and its assertions and indicate possible problem areas. In the same way, a lint program checks for errors in the code's syntax and structure, assertions can be used to check for errors in the design's behavior. Assertions provide many benefits to system-level engineers, design engineers doing RTL coding, and verification engineers. Each group brings different knowledge about the design and its operation, but a common assertion methodology allows all parties to benefit.

Assertion Definitions

To understand more details of an assertion-based methodology, a common set of definitions is presented.

Property: A general behavioral attribute used to characterize a design. Properties can be high-level attributes, such as characteristics of incoming and outgoing networking packets or low-level attributes related to the state encoding of a finite state machine (FSM).

Event: An occurrence of a desirable behavior. Observing events is required as part of verification to ensure completeness. Measuring the occurrence of events leads to quantitative data about specific corner cases and indicates that other properties of the design have been verified. Statistics about events lead to functional coverage metrics.

Assertion: An assertion is a statement about a specific property that is expected to be true for the design. Assertions are most often used to trap undesirable behavior. Assertions are checkers and monitors used to enforce rules and assumptions about the design.

Static: An event or assertion that is true for all time or is only checked at a specific instance of time. No knowledge of previous history of the design state is required.

Temporal: An event or assertion that spans a sequence of time. History is required to track the sequence over time.

Procedural Assertion: An assertion described within the context of an executing process or set of sequential statements, such as a VHDL process or a Verilog always block. The assertion will be evaluated based on the path taken through the set of sequential statements.

Declarative Assertion: An assertion that exists within the structural context of the design. It is evaluated along with all of the other structural elements in the design, for example, a module that takes the form of a structural instantiation.

Regular Expression: A regular expression is a way to express how a computer program should look for a specified pattern and how to react when matching patterns are found. A common use of regular expressions is found in the UNIX grep tool. Specification of properties is easily done using regular expressions. This explains why languages such as PERL are used in design verification applications.

Property Language, Declarative Language, Assertion Language, Formal Property Language: All of these languages are used interchangeably to describe a language that can be used to describe high-level design specifications, properties, events, and assertions. These languages are designed to provide a concise format for complex temporal sequences and regular expressions.

Assertion Approaches

Five approaches to assertions have been described in the literature:

• Declarative Assertions using a library of Verilog monitor modules
• Procedural Assertions using a Verilog assert construct
• Formal property languages
• Pseudo-comment directives
• Post-processing simulation history

As of this writing, various theories about which methodology is best for assertions are fragmented. The goal here is not to promote one versus another, but to introduce each and list some of the commonly documented pros and cons. The examples used are not meant to be comprehensive, but they do cover some of the more widely discussed methods.

Declarative Assertions

The most common methodology for assertions today uses the declarative assertions in the Open Verification Library (OVL), which is freely available at www.verificationlib.org. OVL is an assertion monitor library of Verilog modules that can be easily instantiated into a design. OVL provides a consistent way to specify static and temporal assertions in RTL code. OVL provides a unified message reporting mechanism that can be easily customized for specific projects by changing very little code. It also provides an easy way to enable and disable assertions during simulation. OVL also provides a consistent severity level scheme that can be used to stop simulation on fatal errors. Work on OVL is continuing with approximately two new releases per year. OVL will continue to evolve as related standards stabilize. OVL is very easy to use and is a good first step in getting started with assertions. It is available now and has been proven and used on many projects. Its open source format makes it appealing since it can be customized for each application. Since OVL uses a library of modules, the assertions must be instantiated into the design. The one capability it does not currently have is procedural assertions, which are sometimes called in-context assertions.

Procedural Assertions

Instead of instantiating a module from a library, sometimes it is more convenient to specify assertions using procedural statements. Such is the case with the new assert construct that is part of the SystemVerilog 3.0 specification approved by Accellera (work is continuing in SystemVerilog 3.1). Procedural assertions are useful in the context of a Verilog always block with procedural code, such as a case statement or an if-then-else block. Procedural assertions can be inserted into the code, depending on which branch has been taken. This allows the assertions to be active during the context in which they are important. Both declarative and procedural assertions are good ways to capture design intent during the RTL coding process. If they are not captured during this phase, the knowledge is probably lost since it is unlikely anybody will go back to insert these assertions.

Formal Property Language

The next method used for assertions employs a formal property language. These languages are constructed for the purpose of specifying design properties with minimum effort. They are very powerful in creating complex temporal expressions, and they also make use of regular expressions to allow complex behavior to be specified with very little code. These languages have existed for many years, but have not been used in mainstream design. Current examples are Sugar, which is being used by the Accellera formal verification committee, and the Open Vera Assertions (OVA), which is being used by Synopsys for formal verification tools, as well as in the VCS logic simulator. Formal property languages are useful during all phases of the project and at all levels of design. System architects can use these languages to specify high-level properties of the design. They can be used by verification IP Based SoC Design 2002 - October 30-31, 2002 4 engineers to perform black-box verification without understanding all of the details of the design and by RTL designers to specify low-level assertions about the code. One point that has previously been confusing about assertions is the relationship between the formal property language and procedural assertions, such as the SystemVerilog assert language construct. Certainly, there is much overlap since both can be used to specify assertions. The formal property language is more general purpose, not tied to any specific language issues of Verilog or VHDL. Over time the syntax used to specify properties will converge so that a single syntax can work for both a formal property language and HDL language extensions. If this is not possible due to constraints of the Verilog namespace, at least the syntax should be very close. Currently, tools using a formal property language for assertions usually put them into a separate file so formal tools and simulators can process them separately.

Pseudo-Comment Directives

Another approach that has been taken to specify assertions is the use of pseudo-comments. By embedding assertions in comments, they can be put directly into the RTL code and will not interfere with the Verilog syntax or require any changes to the simulator. Formal verification tools can read the comments using a special parser. In addition to formal methods, these tools can also output a Verilog RTL equivalent for each assertion that allows the assertion to be simulated and flagged in a standard logic simulator. This instrumentation process is useful since it can automatically gather functional coverage metrics about events and assertions during a simulation run, create a database of activity, and display the activity in a concise format for users. Data from multiple simulations can even be merged to form a complete picture of functional coverage. The methodology is similar to the instrumentation process commonly used in code coverage; 0-In Design Automation is working in this area.

Post-Processing Simulation History

So far, all of the methods described have done assertion checking during simulation. A different approach is to check for assertions after a simulation test is complete. In the same way engineers use waveform dumps to debug a problem after the simulation is complete, they can check for events and assertions. TransEDA has developed a tool that can read a waveform file in VCD or FSDB format, read a set of assertions specified in PERL or Sugar, and provide information about the assertions during the simulation run. This methodology does not require any changes to the simulator, any language extensions, or any changes to the design files. Depending on the number of signals needed and the length of the simulation, large waveform files could be required.

Technology and Goals for Assertion-Based Methodologies

An approach of assertion-based methodology is ReConfigurable Computing (RCC) technology by Axis Systems. RCC shortens long simulation times and increases simulation productivity by providing advanced debugging features, such as simulation hot swap and VCD-on-Demand, that allow engineers to quickly find problems. Enabling a consistent methodology throughout simulation, acceleration, and emulation, RCC provides the highest simulation performance and the ability to run behavioral code, such as $display and PLI.

As designs get larger and larger, they will require some form of acceleration and/or emulation to achieve verification goals. By enabling faster simulation that works well with assertions, users can leverage both of these emerging technologies to meet project goals. Historically, the value of emulation was raw performance. Emulation users have suffered greatly from poor visibility during emulation. Unlike simulation, emulation does not allow testbench and monitors to report activity in the emulator. Assertions are a way to provide this visibility. An efficient implementation of assertions maintains the performance value of emulation and provides the visibility to significantly improve emulation debugging. Certainly, running faster is helpful, but if engineers have to remove assertions during emulation, all of the aforementioned benefits of assertions are completely lost.

Assertion Processor

Assertions can be decomposed into two parts: detection and failure processing. Assertion detection is done using state machines. All of the temporal expressions that are used to write an assertion can be implemented in the form of an RTL state machine. By definition, RCC can run all assertion detection in RCC hardware at hardware speed. Similar to a microprocessor interrupt, Assertion Processor receives interrupts when assertions fail and activates a software service routine that runs on the workstation and has access to behavioral code, such as $display or PLI. Assertion Processor allows engineers to maintain the use of assertions from simulation to simulation acceleration and into emulation without being forced to remove them or execute assertion detection in software simulation. Assertions become a valuable debugging tool in the historically difficult-to-debug emulation environment.

The interrupt-driven implementation of Assertion Processor is more efficient than polling for assertion violations from a software testbench and does not impact emulation speed when there are no assertion violations. Polling requires many bits inside the emulator to be read every clock cycle. If the design contains 10,000 assertions, then an equal number of bits must be read every clock cycle. Then, the bits have to be examined to find out if any assertions have been triggered, and if so, the appropriate assertion processing code is executed. Testing by Axis has shown polling to be four times slower than an interrupt-driven implementation. The interrupt-driven architecture provides the required visibility and the performance of assertion detection in hardware. The added advantage of the RCC engine is its event-based algorithm. Assertion Processor accurately handles assertions that are not sampled on clock cycle boundaries because of the event-based algorithm of RCC. Cycle-based algorithms and polling on clock cycle boundaries cannot handle these types of assertions.

For fatal assertions, control is required to stop the simulation instead of wasting simulation cycles. This can be done from the software service routine using ordinary Verilog commands, such as $finish.

Another feature of Assertion Processor is the ability to configure it to perform simulation hot swap and stop during assertion processing. Not only does swap and stop allow behavioral code to be run, but it gives a user source-level debugging and full access to all of the signals of the design. Some engineers prefer to use this interactive style of debugging instead of exiting the simulation and using post-processing debugging tools. After debugging is complete, the user has the option to exit, to continue to run in the software simulator, or to use simulation hot swap to load the simulation back into the RCC engine and continue.

As an example of using Assertion Processor, consider the assertion shown in Figure 1. This assertion can be coded using the assert_change module from OVL, as shown in Figure 2. To allow OVL to map to RCC to get the benefits of the $display assertion reporting, the ovl_error task in ovl_task.h is customized. When the assertion fails, the display_task will be executed in software on the workstation so the $display is visible and entered into the simulation log file as usual. A diagram showing how assertion-processing works is shown in Figure 3.

Users achieve the highest debugging productivity by combining Assertion Processor with VCD-on- Demand (VoD) to generate waveform information. VCD-on-Demand (VoD) alleviates the limitations associated with large waveform files and the struggle to decide when to dump and what to dump into waveform files. Users can run without specifying any dumping, and after the run is complete, they can go back to produce a waveform file for any desired window of simulation time and any scope of the design. Assertions pinpoint design errors, and VoD provides the most efficient way to produce waveforms starting at the point of assertion failure and working back to the root cause of the problem without re-running simulation. A diagram showing the debugging flow with VoD is shown in Figure 4.

Axis is currently working with multiple assertion methodologies to ensure that they run well with Axis products, providing the highest possible performance and debugging efficiency. Details of specific assertion methodologies and associated design flows will continue to be documented in white papers and application notes for users seeking the highest performance verification platform combined with the latest assertion-based design and verification techniques.

Summary

Assertion-based verification methodologies are the next breakthrough in design verification. When this methodology is combined with a high-performance verification platform, design teams can meet the challenges of the next generation of complexity. An introduction to assertions has been provided, and the benefits of such methodologies have been applied to general logic simulation, as well as to the specific RCC verification platform from Axis. A methodology has been described that leverages the emerging set of formal verification tools, as well as the high-performance simulation tools from Axis. Assertion count in today's ASIC designs typically ranges from 1,000 to 10,000 and incurs a ten to fifteen percent simulation performance penalty. With RCC technology and Assertion Processor, assertion detection executes in parallel with the design, and assertions incur no simulation performance overhead. By accelerating the design and the assertion detection, users get the highest level of simulation performance while maintaining the increased observability provided by assertions with no change in design flow. Efficient assertion processing that uses an interrupt-driven implementation also maintains high performance when assertions fail.

By providing the only general purpose platform that can accelerate assertions of many types, Axis is leading the way in promoting the write-once, runanywhere characteristic of assertions and enabling assertions to be adopted during all phases of the design cycle. Axis is the technology leader in IP Based SoC Design 2002 - October 30-31, 2002 6 simulation productivity with its Assertion Processor, VCD-on-Demand, and simulation hot swap for advanced simulation control and visibility. Axis is providing an open system and is working to support emerging assertion standards and methodologies and will continue to educate and promote the use of assertions as standards emerge and methodologies evolve.

References:
[1] T. Fitzpatrick, H. Foster, E. Marschner, P. Narain, "Introduction to Accellera's assertion efforts", EEdesign, June 2, 2002
[2] Synopsys, Inc., "Assertion-Based Verification", May 2002
[3] H. Foster, "Improving Verification through Property Specification", D&R Industry Articles
[4] J. Emmitt, "Verifying complex SoCs with OVL", Electronic Engineering Design, January 28, 2002
[5] 0-In Design Automation, Inc., "Black & White Assertion-Based Verification Flow", The Verification Monitor, May 2002
[6] L. Bening, H. Foster, Principles of Verifiable RTL Design, Kluwer Academic Publishers, 2001
[7] J. Bergeron, Writing Testbenches Functional Verification of HDL Models, Kluwer Academic Publishers, 2000