Verification tools and methodologies have both evolved and undergone revolutionary changes, and both are equally as important to stay abreast of Moore’s law. Complex SOC designs can be implemented by acquiring third-party intellectual property (IP), a divide and conquer approach within development teams, and, of course, by adding more designers. Verification, on the other hand, must deal with the large designs as a whole. This burden falls on the underlying verification tools and associated methodologies that must be able to "simulate" a model of the design, often at different levels of abstraction. Fortunately, assertion-based verification enables a revolutionary methodology change that addresses this ever-increasing burden by adding observability (result checking) and testing (development of actual tests) into the verification environment.
Methods for result checking
Traditionally, several methods have been employed to determine if the simulated model behaves as expected – some that check for correctness during simulation and others as a post-simulation batch process. Some examples:
· Check against a reference model (simulation run-time). A reference model, usually at a higher abstraction level, is run in parallel with the design model and operation is compared in real-time.
· 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.
· Assertions (post-simulation or simulation run-time). Assertions are pieces of code that concisely express desired or undesired behavior, often written in specialized language such as SystemVerilog Assertions (SVA) and PSL. Simulators read these descriptions along with the model and perform the checks at run-time. Post-simulation checkers are most efficient when deployed in batch-mode.
Introduction to assertions
Assertions provide a concise description of the design specification separate from the RTL design implementation. Assertions can be coded using traditional languages such as Verilog, VHDL, or C and have been for a number of years. But 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. Specialized languages such as SVA are designed to describe such assertions more 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.
· At the lowest level are Boolean expressions of design signals that become the building-block "components" for sequences.
· Next come Sequences that are a list of Boolean expressions in a linear order of increasing time.
· On top of sequences are Properties that combine the sequences in various ways.
· At the top-most level are Directives (e.g. assert) that indicate what to do with the properties.
Below is an example that shows this hierarchical building-block approach.
sequence c_l;
@(posedge clock) (bus_mode == ‘INCA) && PC_load;
endsequence
property e_INC;
@(posedge clock) e_l |-> e_r;
endproperty
CF_COVER: cover property (add_overflow);
INCPC: assert property (e_INC);
Efficient assertion methodology
While assertions can be checked dynamically or statically (formally), let’s focus this discussion on 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 (data required for debug and analysis) can have a severe impact on simulator performance. The temporal nature of assertions can spawn multiple attempts and threads in parallel, significantly increasing the run-time and memory consumption of the simulation in order to capture the support data necessary for later debug and analysis. Shifting the bulk of the work to the debug system, which, in turn, can be optimized to calculate only the relevant data can alleviate the run-time burden. In this way, the debug system automatically generates the support data as needed, and the simulator can perform the checks much more efficiently. Ideally, the debug system also checks the assertions against the signal data captured during simulation, so the simulator doesn’t need to perform additional work in support of assertion checking.
This capability can also be very useful during the assertion development process when assertions can be quickly checked in real-time as they are coded. The alternative is to repeatedly run simulations after every small change in the assertion code, which can be very time-consuming.
Debug in an assertion-based verification environment
Because the debug of assertion failures poses many challenges, a debug system needs to include the following capabilities:
· Assertion source code debug with tracing between properties, sequences, events and the design;
· Navigation of assertion components and advanced searching and filtering;
· Capture of assertion results from simulators into database for post-simulation debugging;
· Off-line checking of assertions based on captured signal data, i.e., without dependency on simulator;
· Visualization of assertion results in waveform and within context of source code;
· Appropriate handling of local variables so engineers can quickly see the value of the local variable for the particular attempt or thread they are debugging; and
· Tagging mechanism that allows engineers to quickly jump to the design signals impacting an assertion.
Assertion debug
Once the design description, assertion source code, and signal and assertion results are loaded into the debugger, all of standard capabilities available in modern debuggers can be applied to debug assertion source code and results.
Tracing within assertion code and between assertion code and design code is a key requirement. When debugging a failure, engineers need to be able to jump from the assertion directive statement to the property description; then to the sequence description; and so on down the hierarchy all the way to the design signals. This creates an intuitive process for quickly tracing up and down the assertion building-block hierarchy that is aligned with the way engineers think about and code assertions.
Results from assertion checking can be displayed within traditional waveform views using notations appropriate for assertions. Some advanced debug tools include mechanisms to visualize results within the context of the source code.
While traditional debug views provide value to an assertion-based methodology, completely new capabilities are required to address assertion-specific requirements. In an assertion-based verification environment, it is common to start debug at the point of assertion failure. To eye-ball failures in the waveform view is not practical. More flexible views such as spreadsheets enable engineers to customize and sort the data to quickly identify the failure points. This tabular view could effectively serve as the “cockpit” for an assertion-driven flow.
Automation
Thus far, we have been illustrating how traditional debug capabilities such as source code tracing, waveforms, etc. can be applied to assertions. Beyond these basic requirements are many opportunities for continued innovation (in automation) to address the unique nature of assertions as well as the challenges engineers face while debugging assertion failures. Debugging an assertion failure involves analysis of structural, logical, and temporal information. Engineers must jump from the source code to the waveform to get the correct data, and then manually calculate the values in property statements. This process is time consuming, error prone, and includes many manual steps.
In order to automate the tracing and root-cause identification of an assertion failure, advanced debuggers incorporate analysis engines to calculate all the relevant values as needed in property statements using data already available in the trace file. The debugger infers the behavior of the assertion from the source code. Once the data has been calculated, the engine can automatically trace over time from the failure to the root-cause (keep in mind that it already understands the behavior of the assertion). In essence, the engine automates the tasks that are manually handled by engineers today when debugging assertion failures.
The lowest level of the assertion hierarchy typically comprises boolean expressions of design signals. An analysis engine might also analyze expressions and sub-expressions and automatically present their "value" ("true" or "false"). The ability to quickly see which expression is false can help engineers get to the design signal causing the failure much faster. Once the cause is isolated, the signal can be traced within the design using standard and advanced debugging techniques.
Summary
Assertions and assertion languages provide a concise mechanism to check for undesired design behavior by adding observability and testing into the verification environment. Assertions can be checked dynamically or statically (formally). Dynamic checking, either by a simulator or post-simulation assertion checking engine, enables engineers to quickly enhance their verification flow with assertions. Fortunately, advanced debuggers (such as SpringSoft’s Verdi™ Automated Debug System) also have been enhanced to help engineers adopt an assertion-based methodology using specialized languages such as SVA. They also offer analysis engines geared towards assertion debug that both simplify and accelerate the process of locating the root-cause of assertion failures, whether in the assertion code or design.
Captions
Traditional debug views have to be extended to work with assertions.
SpringSoft’s Verdi Assertion Analyzer automates root-cause analysis for assertion failures.
Click here for the illustrations:
Figure 1, Figure 2
