SystemVerilog Assertion Backgrounder
Verification tools and methodologies have both evolved and undergone revolutionary changes, and both are equally as important. Without a doubt, simulators and support tools have evolved to keep pace with the incremental requirements (primarily increasing design size). However, it is the revolutions that provide the significant increase in productivity necessary to stay abreast of Moore's Law. While the hoopla around Moore's Law has traditionally been around advances in semiconductor technology, it is worth noting that whatever you build or want to build has to be verified (unless of course all you are going to build is memory).
Complex designs can be implemented with a divide and conquer approach - and of course by deploying more designers. Verification, on the other hand, must deal with the large designs (often extremely large) as a whole for which the burden primarily falls on the underlying verification tools and associated methodologies. These tools must be able to 'simulate' a model of the design, often at different levels of abstraction (register transfer level, gate, etc.). Fortunately, assertion-based verification enables a revolutionary methodology change that addresses this burden through enhanced observability (result checking) and testing (development of actual tests).
Methods for Result Checking
The tool or a human has to determine if the simulated model behaves as expected. Traditionally, several methods have been employed to do this with some that check for correctness during simulation and others as a batch post-simulation process. These include:
-
Check against a reference model (simulation run-time). In this process, a reference model, usually at a higher abstraction level, is run in parallel with the design model, and operation is compared in real-time. High-level testbenches are usually structured this way.
-
Comparison with expected operation (post-simulation). This assumes that "golden" results have been previously saved, most likely from another simulation run, and possibly from a simulation of a model at a higher level of abstraction. To deal with minor differences in timing and such, smart comparison tools such as Novas' nCompare have been developed to automate this task.
-
Assertions (post-simulation or simulation run-time). Assertions have been around for a number of years but have only recently gained prominence with the emergence of standard, specialized languages such as SystemVerilog Assertions (SVA) and PSL. They are pieces of code (often in a specialized language) that concisely express desired or undesired behavior. Simulators read these descriptions along with the model and perform the checks at run-time. Post-simulation checkers, such as Novas' Assertion Evaluator have been developed to perform the check more efficiently as a batch post-simulation process.
Introduction to Assertions
Assertions can be considered a concise description of the design specification separate from the design implementation description (e.g., Register Transfer Level, or RTL). Assertions can be coded using traditional languages such as Verilog, VHDL, or C. However, traditional languages can require many lines of code as well as burdensome 'software techniques' for programming. For example, the explicit use of Verilog 'fork' blocks would be required to describe an assertion that must be checked on all clock cycles, since a particular assertion can and often does span multiple clock cycles.
By contrast, specialized languages such as SVA are designed to describe assertions concisely. Let's illustrate this with a simple example (shown in Figure 1 below). Assume we want to check that "After the request signal is asserted, the acknowledge signal must be asserted 1 to 3 cycles later."
Figure 1
Note the use of the Verilog 'fork' and 'join' pair to model the temporal nature of this behavior. On the other hand, SVA provides specialized syntax to deal with this in a more concise manner - the ## means 'followed by specified number of cycles later'. The number of cycles can be an absolute number or a range as in the above example. Other more complex variations are also possible, while the equivalent Verilog description would be nearly impossible to code and understand. By virtue of the @(posedge clk), the assertion check 'fires' on all clock edges, which in turn means that multiple copies (called attempts) of the above check might be running in parallel at any point in time (i.e., before the first check is done evaluating, the next one starts). It is clear that an assertion language such as SVA is an absolute necessity to model this kind of behavior accurately and concisely.
Writing Assertions
Like designs coded using hardware description languages (HDLs), assertions are best described hierarchically. This promotes ease of coding, ease of understanding, and reuse, among other things. Hierarchy is illustrated below in Figure 2 using SVA terminology. At the lowest level, boolean expressions of design objects (signals) are created and become the building-block 'components' of sequences. Sequences in turn become the building blocks of properties. At the top of the hierarchy, directives indicate what to do with the properties.
Figure 2
Below is an example that shows the hierarchical building-block approach.
Like HDL-based design coding, the hierarchical-based approach is more natural to engineers. Ideally, some amount of assertion code should be in-lined with the design code, which implies that it should be written at the time that the design is being coded. In effect, this allows the designer to code the specification of the design in the higher-abstraction assertion. This "specification" can then be automatically checked during verification.
Of course, assertions can also be written at a later stage and separate from the design description itself. This allows assertions to be coded by a separate group (perhaps a team of verification engineers), and also decreases the barriers to entry for design and verification teams by allowing the newer assertion methodology to be applied to existing or older designs without meddling with the existing design code.
Benefits of Using Assertions
Special-purpose assertion languages provide the obvious benefit of conciseness to enable the verification task at hand. From a methodology point of view, assertions also provide many additional and equally important benefits that include:
-
Powerful mechanism for adding observability and testing into verification environments, e.g., assertions can be "hooked up" to points of interest in the design targeted for "probing".
-
Higher level of abstraction than the design - specification rather than implementation that can be checked automatically by dynamic or static (formal) verification tools.
-
Flexible methodology that works out-of-the-box with existing flows and allows code to be in-lined in the implementation or external.
-
Ideal mechanism for delivery with intellectual property (IP) so users can ensure correctness when integrating into their system. Additionally, assertions can be used to provide a quality metric of the IP in terms of coverage.
An Efficient Assertion Methodology
Assertions can be checked dynamically or statically (formally). For the purposes of this discussion, we will focus on methodologies that incorporate dynamic (simulation) checking. Most commercial simulators already support or are close to supporting standard assertion languages. While simulators generally fare well with simple assertion checking, the run-time acquisition of 'support' data can have a severe impact on simulator performance. Support data relates to the values of properties, sequences, and local variables - data that is generally required for debug and analysis when an assertion fails. Therefore, the assertion-based methodology would benefit greatly when used in conjunction with debug systems that can take on some of the tasks traditionally reserved for the simulator.
The temporal nature of assertions can spawn multiple attempts and threads in parallel, significantly increasing the run-time and memory consumption of the simulation when capturing support data. One way to alleviate this run-time burden is to shift the bulk of the work to debuggers that are optimized to automatically calculate only the data of interest as needed. In this way, the simulator can focus on the checking function and run much more efficiently.
In the ideal scenario, the debug system also checks assertions against the signal data captured during simulation. Using this approach, the assertions can be used as a specification to "data-mine" the design behavior captured in a signal trace file, which is already available in the typical verification methodology. This capability is also very useful during assertion development when assertions can be quickly checked in real-time as they are coded. Otherwise, designers must run simulations after every small change in the assertion code, which is very time-consuming.
Debug in an Assertion-based Verification Environment
Debug of assertion failures poses many challenges. First, an assertion failure can be due to a design error or to an error in the assertion description itself. The latter is quite common during the assertion development phase. The multiple attempts and threads of assertions add levels of complexity that require users to correlate large amounts of related data.
Novas is a leading-edge provider of advanced assertion debug and analysis capabilities with its Verdi™ Automated Debug System. Key features include:
-
Advanced assertion source code debug with intelligent tracing of properties, sequences, and events;
-
Navigation of assertion components using advanced searching and filtering capabilities;
-
Capture of assertion results from popular simulators into the Novas Fast-Signal Database (FSDB) format;
-
Assertion Analyzer engine for automated debugging of assertion failures;
-
Assertion Evaluator engine for off-line checking (data-mining) of assertions based on captured signal data (i.e., without dependency on a simulator);
-
Visualization of assertion results in waveform and source code "active annotation";
-
Special treatment of local variables to allow advanced debugging of complex assertions; and
-
"Tagging" of design signals associated with an assertion to allow easy tracing from assertion failure to related design signals/area.
Flexible Assertion Checking
The Verdi system enables users to check assertions using its unique built-in Assertion Evaluator engine or third-party simulators. Assertion checking performed within the Verdi environment uses signal trace information captured during simulation. With third-party simulators, the capture and import of simulator trace information including assertion results into the debug environment is facilitated by FSDB plug-ins (included with the Verdi system). Regardless of the capture mechanism, the full capabilities of the Verdi system are available after the FSDB file containing assertion results is loaded.
Figure 3: Assertion checking flexibility in the Novas environment
Extending the Ultimate Unified Debug Environment
The Verdi debug system brings together the design description, assertion source code, and signal and assertion results for comprehensive debug and analysis. In the source code view, assertions are shown within the design hierarchy using special icons to represent assertion objects such as 'assert', 'cover', 'property', and 'sequence'. Tracing within assertion code and between assertion code and design code is invoked by simple double-click actions. By way of example, double-clicking on a property in the directive statement jumps to the property description; double-clicking of sequences inside properties goes directly to the sequence description; and so on down the hierarchy all the way to the design signals. This ability to quickly trace up and down the assertion hierarchy is a natural extension of the way engineers code and think about assertions, resulting in an intuitive tracing process.
Figure 4: Verdi includes several tightly integrated views and engines for assertion debug
Assertion checking results are displayed within the traditional waveform view using associated notations, such as red down arrows and green up arrows to indicate fail/pass of assertions. More advanced capabilities in the waveform view include a horizontal line indicating the temporal evaluation span of the assertion, i.e., the time between when the assertion started evaluating to the time it eventually passed or failed. While this time can be zero (no horizontal line), for most complex assertions, there is a finite time due to the temporal nature of the code (coded using ## in SVA). The more advanced and popular mechanism for the "active annotation" of results onto source code (first introduced by the Verdi system for HDL debug) has been extended to work with assertion results and objects.
While traditional debug tools provide value to an assertion-based methodology, new capabilities are required to address assertion-specific requirements. The new Property Manager in the Verdi environment provides the "cockpit" for an assertion-driven flow. From this view, users can quickly locate failures with a highly customizable tabular display of results, instead of searching through multiple waveforms. Other engines such as the Assertion Evaluator and Assertion Analyzer also can be invoked or synchronized from within this master window.
Automation
Clearly, much progress has been made in the area of assertions with leading-edge capabilities such as those described proven to be quite useful for assertion-based verification flows. Yet, there is still some manual interpretation and correlation of the relevant data required when tracing an assertion failure.
Assertions usually include complex combinational comparisons and temporal relationships between and amongst properties and signals. Thus, the debug of an assertion failure requires the analysis of structural, logical, and temporal information. Typically, designers have had to go back and forth between the source code and waveform to obtain the data, and then manually calculate the values in property statements. This process is time consuming and error prone.
The Verdi system overcomes this obstacle with its powerful Assertion Analyzer engine that automatically calculates all the relevant values in property statements based on the data already available in the FSDB. "Expand" and "shrink" functions enable designers to disassemble complex property statements into expressions or base elements. The engine then calculates the values (or "contributions") of these expressions or base elements and annotates them with "success" or "fail" in the specialized Assertion Analyzer source code window. This makes it easier for designers to determine where to start debugging the assertion failure and automatically trace the root cause of the failure all the way back to the HDL design. From there, the problem can be further traced over time with the patented Verdi behavior analysis engine and temporal flow view.
Figure 5: Verdi's Assertion Analyzer automates root-cause analysis for assertion failures
As is always the case with Novas tools, this Assertion Analyzer window is tightly integrated with all other views. For example, while tracing the assertion source code, the signals related to the assertion can be automatically added into the waveform view. Observation point and failure expressions are clearly noted on the waveforms to help designers understand where and why the assertion failed.
Summary
Assertions provide a concise mechanism to check for undesired results or undesired behavior and enable users to add "out of the box" observability and testing into the verification environment. The Novas Verdi Debug System provides comprehensive assertion-based debug and analysis capabilities that leverage languages such as SVA to further automate the process of tracing, locating and understanding the root cause of design problems.