High-level assertions in standard SystemVerilog that capture functional requirements efficiently
Assertions are widely regarded as a powerful means to improve verification. They can be used both to quickly detect and find the root cause of corner-case issues through bug hunting, and to deliver high-confidence functional sign-off. The SystemVerilog language, however, allows for many inconsistent, hard-to-review, error-prone, and inefficient coding styles. Assertions capturing low-level intent are usually compact and simple, but assertions formalizing entire operations may become cryptic and difficult to reuse and maintain. Organizations investing in formal verification should adopt a consistent assertion style that ensures optimal performance in formal tools and simulators, and applicability and reusability across a wide range of projects and teams. Crucially, the resulting assertions should also be easy to review against specifications.
OneSpin’s Operational SVA enables formal verification enthusiasts to develop high-level, non-overlapping assertions that capture end-to-end transactions and requirements in a concise, elegant way.
High-level timing view
Complex hardware operations often relate to ordered sequences of cause and effect events that mark crucial stages in the execution of an end-to-end transaction. As an example, consider a DMA controller moving data in a memory space. A timing diagram could describe the transfer of a single data item through a read followed by write transactions over a shared memory interface (see picture).
Using a similar approach, Operational SVA uses the SystemVerilog implies operator to clearly separate cause (light blue signals) and effect (red signals) sequences, even when they overlap in time. The use of conceptual architectural-level states in the operation’s trigger condition enables readability and reusability. Moreover, OneSpin’s TiDAL library of SystemVerilog sequences and properties enables engineers to directly translate event-based timepoints, like ‘t_read_rdy’ and ‘t_write_rdy’, into SystemVerilog; this also applies in the case of events that must satisfy complicated ordering rules and dependent-on-variable wait cycles (see dotted lines in the picture).
Data flow verification
Data corruption, dropping, duplication, or reordering bugs have severe consequences. Local variables in SVA may be used as storage locations to capture the values of data transport signals and manipulate them to implement data checks. However, complex flow rules and limitations may lead to cryptic and inefficient code. In fact, engineers often favor the use of states defined in the RTL modelling layer to keep track of the data stream.
OneSpin’s TiDAL library enables Operational SVA to overcome the risks of using local variables by providing a simple and intuitive mechanism to probe data signals and freeze their values. Freeze variables are used to capture and tag the value of a signal at a specific timepoint, similarly to what is done in timing diagrams (see signal ‘data_i’ at timpoint ‘t_read_rdy’ and signal ‘data_o’ at timepoint ‘t_write_rdy’). Engineers can then safely use these constant variables anywhere within Operational SVA, including parallel and overlapping sequences in either side of the implies operator.
Freeze variables are key to implement high-level data flow checks that naturally integrate within Operational SVA, relieving the user of the intricacies and risks of local variables.
Debugging Operational SVA
Operational SVA describes high-level circuit operations, implicitly covering all possible corner case conditions. These assertions are readable and powerful in uncovering corner case bugs, and they typically exercise large amounts of implementation logic. This is a benefit in many respects, but debugging failures might be challenging. OneSpin’s advanced debug environment automatically leverages Operational SVA timepoints and data probing features to speed up root cause analysis of failures. The waveform debugger detects and marks trace cycles with their corresponding timepoints’ names. Additionally, data signals are also marked at the cycle when their values are probed. This extra information, coupled with the assertion debugger and source code tracing, provides the necessary links between the operational and signal-level views of counterexamples.
Summary
OneSpin’s Operational SVA enables engineers to:
- • Translate functional requirements in a formal and simulation executable format
- Capture entire circuit transactions in a concise and elegant way, similar to timing diagrams
- Achieve 100% functional coverage with high-level and easy-to-review assertions
- Adopt a consistent assertion style that is applicable to a wide range of applications and able to deliver optimal performances for both simulators and formal tools
- Cleanly separate implementation-specific supporting verification code from reusable specification-level code
- Further leverage the assertion set using OneSpin’s GapFreeVerification™ and DV-Certify™ tool for automatic detection of specification omissions and errors, holes in the verification plan, and unverified RTL functions
OneSpin 360 DV-Verify includes OneSpin’s TiDAL™ library of SystemVerilog sequences and properties that enable Operational SVA, along with crucial debug support features and methodology documents.
OneSpin 360 DV-Certify includes the GapFreeVerification™ methodology manual and the tool features for the automated functional coverage analysis and debug of sets of Operational SVA.
Further Reading:
- Read the white paper “Achieving 100% Functional Coverage with Operational SVA”
- Read the white paper “Capturing Timing Diagrams in Operational SVA”
Get in touch!
Develop high-level non-overlapping assertions that are easy to review against specifications. Try OneSpin Operational SVA now!
