Introduction to Assertions for Digital-Chip Verification

As today's designs push past one-million gates and move toward 10-million gates, engineers require new tools and methodologies to verify these devices. Unfortunately, some engineers expect to verify these chips using the same waveform dumps, ad-doc 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 assertion-based verification and making sure assertion-based methodologies work well with the company's products.

Assertions provide a common format for multiple tools. Without an agreed upon 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 a 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 test case developed to verify each feature. Test cases 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 automate the manual process of running a test case, visually verifying that the test has covered the feature and adding the test to the regression suite. Without using assertions, there is often no way to guarantee the test case still exercises the feature as the design evolves. Assertions provide a mechanism to measure functional coverage and to quantify test results.

Assertions ease debug and reduce simulation time. One of the main motivations for assertions is reduced debug 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 debug time by as much as 50%. 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 test 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 upon protocol. This can be crucial, since it is possible for a test case 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 good RTL-coding practice. Assertions are far more valuable than comments alone in a design. Well-commented code makes it easier to maintain the design and to understand its 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 human 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, you can use assertions 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.

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 other properties of the design that 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 usually 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. You do not need knowledge of prior history of the design state.

Temporal: An event or assertion that spans a sequence of time. You need history knowledge to track the sequence over time.

Procedural Assertion: An assertion that is 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. One example is 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 through the use of regular expressions. This explains why languages like PERL are used in design-verification applications.

Property Language, Declarative Language, Assertion Language, Formal-Property Language: All these terms are used interchangeably to describe a language you can use 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.

• 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.

At this time, various theories about which methodology is best for assertions are fragmented. The goal here is not to promote one approach versus another, but to introduce each and list some of the commonly documented pros and cons.

One of the points that has been confusing so far 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 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 that formal tools and simulators can process the assertions separately from the functional design.

References

Jason Andrews is currently a Product Manager at Axis Systems, working in the areas of hardware/software co-verification and testbench methodology for SoC design. His experience in EDA and the embedded marketplace includes software development and product management at Simpod, Summit Design, and Simulation Technologies.

Jason has presented technical papers at the Embedded Systems Conference, Communication Design Conference and IP/SoC, and has written several articles covering HW/SW co-verification, simulation acceleration, and emulation. He has a BSEE from The Citadel, Charleston, S.C., and an MSEE from the University of Minnesota.