Feature

Improving Verification through Property Specification

by Harry Foster

Silicon transistor capacity, the ability to utilize these transistors in a design, and the time required to verify these designs are all considerations that drive our decisions about architecting the next generation system-on-a-chip. While silicon capacity continues to increase along the Moore's Law curve (enabling us to create very large systems), the effort required to verify these larger designs has increased at an even greater, and thus alarming, rate-doubling roughly every 6 months. In addition to rising silicon capacity, our ability to utilize this larger silicon capacity has also increased approximately ten-fold within the past decade due to the widespread acceptance of synthesis technology. However, the ability to verify larger systems has not kept pace. Rather, verification productivity has experienced only incremental improvements during the same period. What is clearly needed in verification techniques and technology is the equivalent of a synthesis productivity break-though. This article explores a verification break-through prompted by multi-level specification techniques.

Systematic Approach to Design

The need for a break-through is certainly not new to the design community. It is interesting to compare the events that led to a systematic approach to software design with the state of hardware design today. During the decade of the 1960s, software productivity was dramatically elevated from a low-level assembly language coding environment through the acceptance of higher level programming languages (for example, FORTRAN, ALGOL). This facilitated the development of interactive, multi-user and real-time systems; which included such complex systems as airline reservations, process control, navigation guidance, and military command and control. Accompanying these new complex software systems, however, were numerous startling problems that had been rarely experienced in the software realm-such as system deadlock, livelock, and forward progress problems. To address these problems, the systematic discipline of Software Engineering emerged, providing a management solution to the ever-increasing system complexity. Large software system houses abandoned the ad-hoc Code→Design→Specify development model for a verifiable systematic approach to design (that is, Specify→Design→Code).


Improving Verification through Property Specification Continued…


Systematic Approach to Verification

During the 1980s, hardware design went through its own metamorphosis, setting the stage for a change in our approach to systematic verification. The productivity in hardware design was dramatically elevated from the process of manually generating schematics, to a process of writing higher-level RTL models. At the same time, synthesis technology emerged as an efficient process to translate the RTL model into a gate-level implementation-resulting in an increase in verification complexity. Although most of today's hardware design teams follow the Specify→Design→Code model, the natural language used in specifications is typically incomplete, ambiguous, and error-prone. Furthermore, these specifications do not lend themselves to automatic verification.

In order to address increased verification complexity, methodologies could be improved with more effective techniques-including a combination of traditional simulation, semi-formal bug-hunting techniques, as well as formal property checking. The unifying factor, and key ingredient for a systematic approach to verification, is property specification.

Currently, Accellera (see www.accellera.org)-whose mission is to drive worldwide standards that enhance a language-based design automation process-is developing a formal property language standard through the efforts of its Formal Verification Committee, which supports top-down, specification-driven design methodologies. In addition, the Accellera SystemVerilog Assertion Committee is developing a standard for specifying RTL implementation assertions directly in Verilog. This will enable bottom-up verifiable design practices-improving simulation-based methodologies while providing a path to formal verification.

These emerging standards will enable designers to specify properties and constraints for formal analysis (for example property checking), specify functional coverage models to measure the quality of simulation, and develop pseudo-random constraint-driven simulation environments derived from formal specifications. At the same time, property specification will improve simulation coverage observability and debugging.


Multiple Levels of Property Specification

Why is Accellera driving two standardization efforts (that is, formal property languages and RTL assertions)? Furthermore, wouldn't a single standard (such as a property language) serve all needs? Although formal Property Languages should be able to provide all the power necessary to express high-level system properties as well as RTL assertions directly within the design, experience shows that a variety of stakeholders in the design and verification flow necessitate a variety of approaches to specify design properties.

The reality of the contemporary design and verification flow mandates a broader look at the abilities and goals of the various stakeholders. The value white-box testing (through assertions) provides over a black-box testing approach has been validated by numerous sources. And, white-box testing can be performed with a formal property language or RTL assertions. However, experience shows that a design architect or verification engineer, whose goal is to validate correct system behavior, needs an expressive means for specifying correct behavior. On the other hand, the design engineer's focus is on implementation RTL using hardware description languages (HDLs) and this requires a convenient mechanism for expressing lower-level implementation properties.

In addition to the dichotomy of goals, this issue also encompasses the areas of expertise of the various stakeholders. Quite often, the verification engineer lacks sufficient in-depth knowledge of design implementation details to provide effective white-box assertion coverage. On the other hand, during the course of RTL development, the design engineer makes low-level assumptions about the design's environment as well as other implementation assumptions. Experience has shown that if design assumptions or concerns are not captured during the process of RTL implementation, then many lower-level implementation properties are lost (that is, they will not be verified). For example, the verification engineer might wish to verify that a PCI bus controller exhibits correct behavior. This can be accomplished by using a higher-level property language to specify correct bus functional behavior. The verification engineer, however, would not specify specific implementation level properties. Continuing with this example, assume that the PCI controller contains multiple state machines. The design engineer's decision to implement a particular state machine as a one-hot versus some other type encoding is irrelevant to the verification engineer-provided that the PCI controller exhibits correct bus functional behavior. Yet, capturing properties of the implementation (for example, one-hot) during the design process provides better white-box coverage and simplifies debug during design reuse.


Improving Verification through Property Specification Continued…


Although formal temporal languages (used to describe finite state concurrent systems) have existed for over 20 years, the difficulty in learning these languages compounded by the lack of tool support, has contributed to their lack of acceptance within the design community. Similarly, experience has shown that difficult forms of expressing RTL implementation properties limit the number of assertions captured during the design process-thus poorer quality of white-box coverage.

Ultimately, the most effective overall approach consists of a combination of higher-level specification using a formal property language and lower-level implementation properties. Assertions directly coded within the RTL, versus maintained separately using a formal property language, simplify the integration of lower-level blocks. Similarly, higher-level formal property languages facilitate verification reuse by providing expressive means of specifying intellectual property (IP) interfaces.

Hence, although there is some overlap in RTL assertion specification, versus formal property language specification, the end user of the particular form of specification is different. Thus, property specification convenience as seen by the design architect, the verification engineer, and the RTL implementer must be a consideration. An effective multi-level property specification methodology can be constructed which combines higher-levels of property specification with lower-level RTL implementation assertions. This approach facilitates both top-down as well as bottom-up verification methodologies.

A Specification-Driven Design and Verification Methodology

In a specification-driven design and verification methodology, the design architect begins by creating a high-level specification for key characteristics of the design (such as communication protocols or complex arbitration schemes). This enables specification consistency checking prior to design and implementation-eliminating architectural bugs.


As the architect partitions the design into block-level components, prior to RTL implementation, block-level interfaces should be specified forming verifiable contracts between multiple block-level components. These formal interface specifications serve as constraint models during block-level formal analysis, as well as interface monitors during simulation. Furthermore, through this process, interface misconceptions between multiple engineers will be resolved prior to RTL coding. The block-level interface specification used for formal analysis can be leveraged in a pseudo-random simulation environment by specifying legal stimulus that can be driving into the RTL model, as well as specifying valid output behavior.

As the engineer begins coding the RTL, assertions for any potential corner case concerns should be added using either the Accellera Open Verification Library or the new SystemVerilog assertion construct. For example, assertions that specify that a queue or FIFO will never over or underflow, (see Figure 1)-or that a set of signals is one hot-or that a specified expression (condition) will never occur-should be embedded directly within the RTL.


 Click to enlarge…
 Figure 1
FIFO Over and Underflow OVL Assertion Example

Conclusion

A multi-level property specification methodology enables designers to keep pace with the rapidly expanding silicon capacity by utilizing new verification techniques. Property specification is a key ingredient in the adoption of new verification techniques. Currently, Accellera (see www.accellera.org) is addressing today's verification challenges on two complementary fronts: a high-level formal property language standard as well as a lower-level RTL assertion construct as part of the SystemVerilog standard. These combined specification approaches will enable both top-down and bottom-up verifiable design practices, enabling the designer to:

Harry Foster is chief architect for Verplex Systems, Inc. Foster has experience developing formal equivalence checkers, ATPG tools, physical optimization tools, and assertions tools and methodologies. Foster is serving as Chairman of the Accellera Formal Verification Committee, which is currently defining a language standard for property specification, and is a member of the Accellera System Verilog Assertion Committee. He is the author of the Open Verification Library (www.verificationlib.org), and has papers published on applied assertion and formal techniques. He is co-author of the book Principles of Verifiable RTL Design, Kluwer Academic Publishers (June 2001). He can be contacted at harry@verplex.com.