While verification of complex systems-on-chip (SoCs) poses an unprecedented challenge, a number of factors lead EDA industry leaders to believe that assertion-based verification will likely be the next breakthrough to address this challenge. This belief is supported by early adopters, who have demonstrated that assertion-based verification reduces simulation debug time by 50 percent. It also enables them to capture design intent in a form that permits self-checking code, which dramatically simplifies intellectual property (IP) integration.
In addition, assertion-based verification supports white-box verification strategies, which improve observability coverage within the design. Finally, assertion-based verification addresses the inherent controllability coverage limitations of simulation by enabling the adoption and use of emerging semi-formal and formal technologies. The key component and necessary ingredient that will drive this assertion-based verification breakthrough is specification.
Recently, the Accellera standards organization took steps to standardize this integral component. Accellera proposed standardization through Sugar, a formal property language. As a declarative property language, Sugar supports top-down (functional, specification-driven) design methodologies, and is well suited for specifying architectural and global properties, as well as defining interface specifications during block-level partitioning.
In addition, Accellera has focused on developing standards for specifying RTL implementation properties directly within the designer's HDL using language and library based approaches. The Open Verification Library (OVL) provides a template for structurally expressing a broad class of declarative assertions within the designer's RTL. The SystemVerilog assertion construct facilitates procedurally specifying assertions during RTL development. Both the OVL and the new assertion construct enable bottom-up (that is, white-box) verifiable implementation practices. Bottom-up verification practices improve simulation-based methodologies and provide a seamless path to formal verification.
When used in conjunction, these powerful and expressive formal property languages enable engineers to:
- Specify properties and constraints for formal analysis
- Specify functional coverage models to measure the quality of simulation
- Specify a pseudo-random constraint-driven simulation environment
Assertion-based verification definitions
Before we define assertion-based verification, we must first define its components -- properties and assertions. A property is a general behavioral attribute used to characterize a design, while an assertion is a statement about a specific property that is expected to hold for a design. The aggregate of assertions associated with a design define the operating conditions and characteristics of that design. Assertion-based verification is a multi-faceted approach to verifying a collection of partial specifications, each of which represents a property of a given design.
A design typically consists of a static, hierarchical structure in which primitive elements interact through a network of interconnections. The primitives may be built-in simple functions (for example, gates) or larger, more complex procedural or algorithmic descriptions (for example, VHDL processes or Verilog always blocks). Within a procedural description, statements are executed in sequence. However, within the design as a whole, the components and communication interact concurrently.
Just as the design itself involves concurrent (declarative) and sequential (procedural) elements, assertions may be either declarative or procedural. A declarative assertion is a statement within a structural context that is always active and is evaluated concurrently with other primitives in the design. A procedural assertion is a statement within the context of a process that is executed sequentially in its turn as the procedural description is executed. In keeping with these definitions of declarative and procedural assertions, the Accellera fornal property language is a declarative form of specification (See Example 1), while the new SystemVerilog assertion construct provides a means for expressing procedural assertions (See Example 2).
Declarative and procedural assertions each have a natural place within the design. Consider the case of a finite state machine, described by a single Verilog always block that contains procedural statements. To express expectations about the computation performed in a particular state, the designer may prefer to insert a procedural assertion directly into the code for that state. However, to express expectations about state transitions observable from outside the state machine, or about successive outputs of the state machine, the designer may prefer to add a declarative assertion in the module in which the state machine is defined.
In either case, the ability to embed assertions directly into the code makes it easier for the designer to write assertions that capture detailed design requirements or environmental assumptions, which then become available for the rest of the verification flow. Embedded assertions are also easier to maintain, because they can be updated as the design is updated.
The power of using declarative and procedural assertions is harnessed by standardizing a property language. It is integral to addressing increased verification complexity, however, equally important are effective methodology considerations. Recently, monitor-based methodologies have emerged as a technique for unifying traditional and formal verification.
While standardizing a property language is integral to addressing increased verification complexity, equally important are effective methodology considerations. Recently, monitor-based methodologies have emerged as a technique for unifying traditional and formal verification.
The Accellera Open Verification Library (OVL) assertion monitors provide many systematic elements of an effective assertion-based verification methodology. The OVL incorporates a consistent and systematic means of specifying RT-level implementation assertions structurally through a set of concurrent assertion monitors. These monitors provide designers with a template, which guides them to express a broad class of assertions (See Example 3). In addition, these monitors address methodology considerations by providing uniformity and predictability within an assertion-based verification flow and encapsulating the following features:
- A unified and systematic method of reporting that can be customized per project
- A common mechanism for enabling and disabling assertions during the verification process
- A systematic method of filtering the reporting of a specific assertion violation by limiting the firing report to a configurable amount
Finally, the July release of the OVL will capitalize on and unify the new Accellera standards by incorporating the new Accellera formal property language declarative form of property specification and the new SystemVerilog (and VHDL) procedural form of specification within the library. This will enable designers to take advantage of emerging tools that support these emerging standards-while educating designers (through example) in how to create their own Sugar or SystemVerilog assertions.
Assertion-based verification: principles and application
The utility of the new standards is best understood in the context of a design paradigm. With the increase in design complexity, a more predictable and systematic approach to design is emerging. In this approach, a system is developed from a Specification with iteration through incremental steps of Design-Implement-Integrate-Refine-Design. Typically, a vertically integrated functionality is first developed and then incrementally refined throughout the process until product completion.
A typical design project is staffed with engineers with diverse roles and expertise. In the beginning, design architects evaluate various architectural tradeoffs and establish the high level specification of the design. Subsequently, design engineers evaluate the various design options to implement the design. Concurrently and subsequently, verification engineers verify the implementation for correctness and compliance with the architectural goals.
The diversity of these tasks requires complex and multi-faceted tools and methodologies. A declarative language like the Accellera formal property language is ideal for an abstract high-level specification of the design functionality. This enables the architects to create unambiguous specifications that can be verified using simulation and formal techniques. Furthermore, these specifications can serve as references for verifying the design implementation. Also, verification engineers engaging in black-box verification can conveniently enter design behaviors declaratively to verify the design.
The design engineer may exploit either declarative or procedural assertions by embedding them in the design for the following purposes. Declarative forms of assertions are appropriate for describing behavior that is naturally concurrent-in particular, behavior that involves multiple independent primitives (for example, block-level interfaces). Alternatively, procedural assertions are appropriate for describing behavior that is transient (for example, temporary state during an algorithmic computation).
For the design architect and verification engineer, declarative assertions are natural for capturing top-level requirements and for specifying global behavior (for example, black-box external behavior for IP). Verification engineers are not likely to add embedded assertions, either declarative or procedural, to the design unless they have unusually good insight into the details of the design, and permission to modify it.
However, a verification engineer may take advantage of both declarative and procedural assertions during the course of verification. Architect-supplied external and global assertions may drive overall system verification, while designer-supplied embedded assertions will provide greater visibility (observability) into the design during system verification. Assertion-based verification, which combines both declarative and procedural forms of specification, dramatically reduces the overall verification effort while improving the coverage quality.
The designer, however, might find SystemVerilog assertions natural for expressing properties deeply nested within procedural code. The designers perform a great deal of analysis, simplification, and organization of the design for implementation, which is created in procedural HDL. SystemVerilog assertions provide the ability to insert the assertions appropriately in the control flow when using Verilog. This leverages the design effort and maintains the familiar language environment for the designer. In addition, this enables the verification engineers to conveniently develop their customized library of assertions.
Finally, the HDL assertions are further empowered by OVL, a standard library of assertions. This provides pre-packaged and pre-verified complex assertions along with a consistent method of reporting and controlling assertions during simulation. Also, OVL supports both Verilog and VHDL designs.
Leveraging specification and implementation
It is envisioned that a rich collection of methodologies and tools will emerge that will combine higher-level specification using a formal property language and lower-level implementation properties. . Formal property languages, such as Sugar, provide expressive means of specifying interface behaviors prior to implementation, while the SystemVerilog interface block provides a convenient mechanism to encapsulate the connectivity and protocol between modules during RTL development. Embedding procedural and declarative assertions in an interface is a convenient and powerful way to encapsulate IP interfaces, facilitating reuse of both design and verification information.
A formal specification can be checked for consistency prior to design and implementation-eliminating architectural bugs. This can then be used for top-down verification. The inline assertions facilitate correct design and shorten the incremental design and refinement phases. Formal specification of block-level interfaces provides constraint models during block-level formal analysis, as well as interface monitors during simulation. Furthermore, the block-level interface specification can be leveraged in a pseudo-random simulation environment for generating legal stimulus for the model.
Whether the design and verification methodology is viewed as "top-down," "bottom-up," "white-box," or "black-box," the advantage of these multi-compatible assertion mechanisms is that they provide each contributor with the tools needed to specify a property of the design in a way that is consistent with an environment that is familiar to the engineer. As importantly, the coordination of efforts within Accellera ensures that each mechanism embedded by one stakeholder may also be referenced by others. This avoids the problem of having to specify the same information more than once, with the attendant risk that the two specifications may be inconsistent.
Another advantage of this methodological consistency is that it facilitates the exchange of verification information between cross-functional teams. Assertions embedded in the design notify the verification engineer of the designers' intent, without the need to understand the details of the design itself. With a common semantic for specifying sequences, both groups can simplify assertions by referring to sequences defined by the other.
Just as the OVL encapsulates higher-level concurrent assertions, the next step for SystemVerilog is to add language enhancements to allow higher-level encapsulation for procedural assertions. Such a procedural library will encourage a consistent methodology that enables users to share common higher-level assertions without coding them from primitives. Having this procedural library cover the same set of functionality available in the concurrent OVL provides a consistent toolset from which the designer may choose the most appropriate. The common semantic primitive available to implement these libraries also simplifies the implementation for tool vendors.
Property specification is the key component that will drive assertion-based verification. Accellera is driving the breakthrough in assertion-based verification through its efforts to standardize Sugar, SystemVerilog assertions, and Open Verification Library.
Tom Fitzpatrick is the Director of Technical Marketing at Co-Design Automation, Inc. Tom is Co-Chairman of the Accellera Assertions committee, which is responsible for standardizing the procedural assertion construct in SystemVerilog, and the OVL. He is also a member of the Accellera SystemVerilog committee as well as a member of the IEEE 1364 Verilog Working Group.
Harry Foster is Verplex Systems, Inc., Chief Architect. Harry is serving as Chairman of the Accellera formal property language committee, which is currently defining the Sugar language standard for property specification-and is creator of the Open Verification Library (OVL). He is co-author of the book "Principles of Verifiable RTL Design," Kluwer Academic Publishers.
Erich Marschner is a Senior Architect at Cadence Design Systems, where he is responsible for advanced functional verification product design. Erich has been actively involved with language and tool development to support assertion-based verification for more than 15 years.
Dr. Prakash Narain is Founder and CEO of Real Intent, Inc. He was the project leader for test and verification for UltraSPARC IIi, at Sun Microsystems. He was an architect of the Mercury Design System that was a top-ten AMD goal for 1995. He has architected and developed CAD tools for test and verification for IBM EDA. Dr. Narain has a Ph.D. from the University of Illinois at Champaign-Urbana.