Design-for-verification (DFV) using assertions has received much attention in the recent technical press. Coverage has ranged from standardization efforts for assertion languages to complete DFV methodologies that combine simulation-based flows and formal analysis-based flows.
In this article we show how DFV, including the use of assertions, can extend into hardware-assisted simulation flows. We describe how synthesizable assertions, such as those in Accellera's SystemVerilog standard, carry forward into acceleration and emulation-based flows, and provide valuable feedback to designers even when their designs are placed in real-world environments.
We describe the mechanisms that need to be in place and show how, through leveraging the Standard Co-Emulation Modeling Interface (SCE-MI) standard, a broad solution can be provided.
Introduction
The challenges of verifying today's complex system-on-chip (SoC) designs have been publicized in many places. 120 nm, 90 nm and smaller technologies enable the design of astonishingly complex chips that can no longer be effectively verified through dynamic event-level simulation techniques alone. Hence, we have seen an increased focus on new verification technologies in the last few years to address this "verification crisis."
One approach that has been embraced by many leading companies is the design-for-verification (DFV) methodology. A key component of this methodology is the rigorous use of assertions throughout the design and verification process. Assertions are used to specify design properties and design assumptions, and are subsequently used in both simulation and formal flows to help designers find and eliminate bugs in their designs.
Assertions were pioneered through specialized formal languages and the classical hardware description languages (HDLs) Verilog and VHDL. With the increased adoption of DFV, dedicated assertion languages were developed. The developers of SystemVerilog leveraged this experience to extend Verilog HDL with specific built-in language constructs describing assertions and properties in addition to new design and testbench constructs.
Having a dedicated syntax available for assertions has several benefits. Design properties and assumptions can be captured in a concise, unambiguous way (with at least a factor of ten less code in comparison to an HDL), which makes DFV very practical for both design and verification engineers.
Second, and most important, simulation and formal analysis tools can easily separate the assertions from the RTL. For example, a simulator can automatically monitor the assertions and calculate coverage statistics while a formal analysis tool interprets these same assertions to be properties of the RTL, the validity of which needs to proven.
Another major advantage of having assertions as a built-in feature of SystemVerilog is that the simulator can infer the clock to use for concurrent (synchronously computed) assertions, while avoiding any potential simulation race conditions. Simulation performance can also be much improved from older PLI-based techniques used to implement assertions in HDLs or in separate languages. Since assertions are a native part of SystemVerilog, they execute directly in the simulator along with the design itself.
The only potential downside of having dedicated language constructs for assertions is that the assertions may not carry forward into hardware-assisted verification flows. This is precisely the issue we address in this article. We outline a method by which assertions can be used in hardware-assisted flows and identify further requirements on acceleration and emulation environments to extend the reach of DFV into these flows.
The role of assertions
The heart of any modern verification methodology is an integrated toolset that includes simulation, coverage, advanced constrained-random test generation and formal analysis. Assertions bring all these capabilities together for the user. Assertions are used to drive formal verification, monitor simulation behavior and control stimulus generation, and provide the basis for comprehensive functional coverage metrics. The key role that assertions play is shown in Figure 1.

Figure 1 The role of assertions in a modern verification methodology
Assertions are often used to capture constraints on an interface, precisely defining the set of possible behaviors that are compliant with the protocols executed on the interface. These assertions are then continuously checked during simulation, while the same assertions are analyzed jointly with the RTL to explore the reachability of specific design properties.
Designers developing the RTL code implementing a specific function often make assumptions about how particular submodules behave to achieve the design targets. These assumptions are directly expressed through assertions and continuously monitored for validity. Verification tools can identify conflicts with these assumptions through a mix of dynamic and formal analysis.
Assertions can be used in both "black-box" and "white-box" methods. In the white-box approach, the designer inserts assertions in-line with the target HDL code; these assertions can monitor signals anywhere within the design. In the black-box approach, the assertions monitor only the external interfaces of a specific design module.
This approach is often used by verification engineers to test a module's specifications independently of the designer. It is also used when it is desired to place all the assertion code in separate files, leaving the design HDL code unmodified or, in the case of third-party IP, when the internals of a block may not be well understood or even visible.
Adding up all the assertions that are associated with a module, designers can quickly reach hundreds of assertions that need to be tracked. Automated coverage tools are essential to ensure that all of the assertions are exercised and systematically tracked to guarantee the completeness of the verification.
Combining the individual modules during the integration phase of the project shows the value of having these assertions embedded in the RTL code they automatically carry forward when the full-chip RTL is created. Companies that have followed this methodology have reported thousands of assertions associated with a design that are monitored, in many cases on a cycle-by-cycle basis, while running full-chip simulations.
Simulating assertions in hardware
Many SoC design flows also include acceleration or emulation steps. This typically enables the design to be "simulated" at very high speed, where near real-time data is fed into the chip under test. In the "co-emulation" mode of use, the accelerator/emulator/prototype has a software interface (connected to a software simulator) through which stimulus and control of the simulation can be provided.
In the "in-circuit" mode, the stimulus and response is provided by real-world interfaces or laboratory test equipment such as packet generators or channel simulators. To get the benefit of assertions in these hardware-assisted flows, one possible approach is to have the RTL accelerated, while the assertions (connected to the RTL through the software interface) run in the software simulator.
However, this solution is not practical because it will dramatically degrade the overall system performance. This is because many millions of events may have to be transferred between the design under test (DUT) on the hardware side and the assertion monitors running on the software side for each second of simulated time.
The only reasonable solution is to synthesize the assertions directly into the hardware, which is exactly what has been accomplished in the flow proposed in this article. In this flow, the assertion monitoring function runs together with the RTL at hardware speed, while assertion violations are reported back into the software simulator to aid in the debugging process.
There are three ways in SystemVerilog to handle the reporting associated with assertions:
1. The assert statement:
assert property ( property ) [pass_statement] [else fail_statement]
2. The assume statement:
assume property ( property )
3. The cover statement:
cover property ( property ) [pass_statement]
The assert statement is used to enforce that a property is checked, while the cover statement is used to monitor the property evaluation for coverage. Each of these statements imposes certain requirements on our solution, as well as guidelines for its usage in hardware-assisted simulation flows.
For the assert statement, the SystemVerilog Language Reference Manual (LRM) states that if the property evaluates to true, the pass statement is executed, otherwise the else statement is executed. Each, or both, can be omitted, in which case a call to $error is generated if the property fails.
Practically, this means that both the pass statement and the else statement are to be executed by the software simulator. Reducing the interaction between the hardware and the software simulator to maximize performance leads to the following guideline:
Guideline 1: In assert statements, do not use a pass statement. Use only the else statement, since this indicates an error condition.
The assume statement has no pass or fail statement, and so a call to $error is always generated when the property fails.
In addition to the assert, assume and cover statements, there are also assertion control statements that enable the user to turn selected assertions on and off during a simulation. These controls are primarily beneficial to tune the simulation performance by turning the assertions on only in time slots where problems are anticipated. Since the assertions are already consuming hardware resources, the performance argument does not apply for hardware-assisted verification. This leads to the following guideline:
Guideline 2: Ignore assertion control statements when implementing the assertions in hardware unless false failures need to be suppressed.
The behavior of the cover statement is also defined in the SystemVerilog LRM:
The results of coverage statement for a property shall contain:
- Number of times attempted
- Number of times succeeded
- Number of times failed
- Number of times succeeded because of vacuity
- Each attempt with an attemptID and time
- Each success/failure with an attemptID and time
In addition, any associated pass statement is executed every time a property succeeds.
Clearly, performing the "accounting" functions on the software side would severely degrade the overall performance; hence the ideal solution requires that additional "hardware" be created to perform these functions, which can then be queried at the end of the simulation. The last two items on the above list require storing the attempted and time for each attempt/success/failure. Although providing useful information, this can cause problems in a hardware-assisted flow because of unbounded arrays. We therefore recommend the following:
Guideline 3: Do not implement cover statement accounting functions in hardware-assisted verification; rely on pure software simulation to get this important information for debugging purposes.
Finally, the pass statement of the cover statement will also be implemented in software, and depending on the usage of the property (for example, how many times it is expected to succeed). We recommend not using it, leading to our final guideline:
Guideline 4: In cover statements, use a pass statement only if it is expected to be executed a few times during the simulation.
SystemVerilog immediate and concurrent assertions are synthesizable, enabling a DFV simulation flow with assertions even when using hardware-assisted simulation technologies. Even though additional hardware would have to be generated to ensure the implementation of the cover statement to perform the full accounting of the attempts, successes and failures of the assertions, adhering to a few simple guidelines will ensure a solution that extends the benefits of assertion-based verification into the hardware-assisted simulation flows without giving up performance.
The Standard Co-Emulation Modeling Interface
The previous section outlined the main requirements for a technical solution to extend the benefits of a DFV software simulation flow into a hardware-assisted simulation flow. Next let's explore how a practical, portable (software/hardware vendor-independent) solution can be created.
The key to this solution is the SCE-MI standard from the Accellera Interfaces Technical Committee. This standard defines hardware and software interfaces and services intended for high-performance co-emulation between software test programs and a wide range of hardware accelerators, emulators and prototyping systems.
Although cycle-level or event-level co-emulation is not prohibited by the standard, SCE-MI is optimized more for transaction-level message transfers. In a transaction-level methodology, the test program is written at a relatively high level of abstraction, dealing with complete transactions (such as sending or receiving an Ethernet packet, or a burst transfer on a system bus), rather than pin- and cycle-accurate events. This allows the test writer to be much more efficient in creating test programs.
A separate reusable "transactor" block converts the transaction-level description to the pin and cycle-accurate level required by the desired protocol, using integral state machines or bus-functional models. In a typical SCE-MI-compliant hardware-assisted co-emulation environment, the lion's share of the transactor is developed in synthesizable form so that it can be implemented on the hardware side of the interface, with only an efficient application programming interface (API) on the software side to act as a "proxy" for the hardware transactor.
Since the state machines that expand the transaction-level messages into cycle-level signals are implemented mostly in hardware, and because the hardware-software transport layer only has to transfer messages at the transaction level, the test program can run at very high speeds, taking advantage of the acceleration provided by the hardware. A single transaction message can be expanded into thousands or even millions of clock cycles and pin-level events in the hardware, such as in the case of a 16K-bit 10 Base-T Ethernet packet (extending over several milliseconds of real time) entering a system with a 400MHz system clock.
The standard ensures that tests written for one vendor's environment can be ported easily to another vendor's environment, allowing the end users to preserve their investment in test programs. It also opens the path for third-party transactor providers to create a market for portable, reusable transactor libraries for all the industry-standard protocols such as Ethernet, SPI, USB, PCI, PCI-Express, AMBA and OCB.
Application of SCE-MI to assertions
The standardized infrastructure provided by the SCE-MI is the ideal transport mechanism for the (intended) infrequent failure exceptions produced by assertion statements following the guidelines given above. Furthermore, by using SCE-MI as the transport, the proposed assertion methodology can automatically be used concurrently with transaction-level (or even cycle-level) co-emulation.
The solution is to synthesize the assertions so they can be loaded into the hardware accelerator/emulator/prototype and then to stitch the signals representing the pass/fail status of each assertion to an "assertion monitor" transactor, as shown in Figure 2. This transactor acts as a concentrator, monitoring the results of dozens or hundreds of assertions, and only generating a transaction message back to the software side when needed. Thus, it is not required to bring all the signals monitored by the assertions to the software side on every clock cycle only the failure results when they occur.

Figure 2 Proposed approach for portable hardware-accelerated assertion methodology
In a simple version of this transactor, a message could be generated whenever any assertion fails. A more complicated implementation could classify the assertion monitors and then provide queuing of non-fatal failures. It would only generate a transaction on a fatal assertion failure, when the queue of non-fatal failures needs emptying, or at the end of the co-emulation. Coverage statistics would be transferred at the conclusion of the co-emulation along with whatever was still remaining in the queue.
Since the assertion monitor transactor is only performing a monitoring function, and doesn't have to respond reactively to the DUT, it should be possible to run the DUT in real time or near real time in an in-circuit mode within a prototyping platform while still using the assertion monitor transactor to indicate assertion failures and to report coverage statistics on a (slightly) time-lagged basis to the monitoring software.
This opens the very exciting possibility of not only being able to use assertions with directed and pseudo-random test vectors in pure simulation or co-emulation runs, but also keeping the same assertions at work while the prototype operates in an in-circuit environment. Thus, incorrect assumptions or corner cases that were not stimulated during simulation might be detected and even localized while in-circuit. Other debugging aids offered by the hardware system supplier, such as waveform tracing, could then be directed to the right point in the logic, and triggered at the appropriate time, to maximize their value in debugging the failure.
Results
Aptix performed a proof-of-concept trial of the proposed methodology. In the trial, assertions in the OpenVera Assertions (OVA) language, which represents a subset of SystemVerilog assertion functionality, were simulated using Synopsys' VCS simulator along with a DUT written in Verilog RTL. The assertion code was compiled using a VCS utility that synthesizes assertions into hardware-readable format, and mapped into an Aptix System Explorer prototyping platform, along with the DUT RTL code.
This VCS utility creates a design module with a signal output port for each assertion statement compiled. The signal represents whether the assertion passed or failed using logic '1' and '0' values, respectively. These signals were stitched to Aptix's cycle-level co-emulation interface (Expeditor), transmitted to the software side and presented as waveforms within VCS as the co-emulation was run.
The results of the assertions in the co-emulation mode accurately reflected the results obtained by pure software simulation, validating the approach of compiling and mapping assertion monitors into the prototype platform hardware and transmitting the results of the assertion monitors back to the software side.
While the test case was too small to show detailed performance statistics, projecting the results for a typical project (several million gates plus memory) leads us to expect that the typical performance numbers for Aptix' System Explorer prototyping platform can be retained when the assertions are synthesized and mapped into the hardware and a transaction level or in-circuit methodology is used. Final performance numbers will be highly dependent upon the specific project testbench and DUT, code size and style, and specifically on the amount of data to be sent across the Expeditor interface, which in turn depends on adherence to the guidelines given previously.
Future work will include demonstrating an SCE-MI-compliant transactor to concentrate the assertion signals and report on an exception basis rather than on a cycle basis, as in the results presented. System Verilog Assertions (SVA) will be used in the proposed flow as soon as the VCS assertion synthesis utility becomes available for SystemVerilog.
Clearly, transaction-level co-emulation and in-circuit modes can show many orders of magnitude performance increase over pure simulation, allowing for up to a million-fold increase in the number of verification cycles available on a project. By compiling the assertions into hardware, these large speed-up factors can be retained, thereby extending the bug-finding capability of assertions into the emulation/prototyping domain.
Conclusions
Assertions are becoming recognized as a very valuable adjunct to traditional verification methodologies. They can be evaluated both statically by formal tools and dynamically by simulators. Assertions can work very effectively with classical directed-test verification flows as well as with more advanced techniques, such as pseudo-random test generation and transaction-level methodologies.
The availability of a path from assertions to hardware allows the benefits of assertions to accrue to hardware-assisted verification approaches, such as simulation accelerators, emulators and prototyping systems, by allowing the assertions to be synthesized and dynamically evaluated within the high-performance hardware. This will aid in the tasks traditionally performed by these systems: RTL integration and debug, and early firmware and application software development and integration.
The Accellera SCE-MI specification provides the ideal vehicle for transporting assertion failure messages from the hardware-mapped assertion monitors to software-based tools in a portable, vendor-independent manner while maintaining high performance.
In-circuit use of assertions in prototyping systems, especially, since they typically exhibit the highest performance of all the hardware-assisted platform types holds the promise of identifying errors in design assumptions or in the design implementation that may not be stimulated or observed by other methods.
Furthermore, the distributed nature of assertion monitors and the assertion failure messages can help to quickly localize a fault to a specific logic module and help localize the time the fault started propagating. Debug tools provided with the hardware platform can then be used to help understand and fix the issue in the most effective manner.
SystemVerilog assertions example

Additional reading:
Accellera Standard Co-Emulation; Modeling Interface Reference Manual Version 1.0 (May 29, 2003)
Design for Verification; Blueprint for Productivity and Product Quality
Rindert Schutten and Tom Fitzpatrick (Synopsys, Inc.)
Retargetable Transaction-Based System Level Verification
Damian Deneault and Rich McAndrew (Zaiq Technologies, Inc.), Charlie Miller and Richard Newell (Aptix Corporation)
System Verilog 3.1; Accellera's Extensions to Verilog
Richard Newell is director of Hardware Product Marketing at Aptix Corporation. His previous experience in IC design is now applied at Aptix in creating pre-silicon prototypes based upon FPGA technology, and in helping steer the technical direction of Aptix products.
Rindert Schutten is director of marketing for Synopsys' System Level Solutions Verification Group. He has over 20 years of software development and EDA industry experience. Prior to his current role, he was driving Synopsys' worldwide verification services in the Professional Services organization. In this role, he worked directly with leading companies on creating advanced solutions for their most challenging system-on-chip verification problems.