Hybrid RTL Formal Verification Ensures Early Detection of Corner-Case Bugs April 2003

Introduction
Functional verification continues to consume significant time and resources for product development teams. As design complexity grows, the challenge of finding corner-case functional bugs in the design increases exponentially. According to a number of recent studies, it is well understood that functional bugs are the leading cause for design re-spins.

To address this growing challenge, verification methodology has evolved from manually created directed tests to powerful constraints-driven random stimulus generation techniques. Additionally, product development teams are making increasing use of assertions to flag incorrect design behavior during simulation.

Constrained random verification, used heavily at chip or system-level, is effective in exposing conditions that are impossible to comprehend manually, however the random nature of this methodology makes it difficult to know if the design has been verified adequately. Also, block-level design bugs are difficult to find and hard to debug during chip or system-level verification. Many teams break down full chip verification to multiple, more manageable block-level verification. Extensive block-level verification results in high quality design modules, which can be integrated to create a high quality chip or a system. RTL formal verification products render themselves well to block-level verification. But, they are mostly difficult to use and have significant capacity and performance limitations, making them ineffective for mainstream usage.

This paper presents a new technology called hybrid RTL formal verification that allows engineers to find deep, corner-case bugs, quickly, resulting in shortened verification cycle and high quality designs.

Hybrid RTL Formal Verification
Hybrid RTL formal verification technology finds functional bugs by formally verifying if a given design satisfies a set of properties that define the intended behavior of the design. This paper uses “properties” and "assertions", interchangeably, to refer to declarative statements that define the expected behavior of a design. Tools implementing hybrid RTL formal verification architecture combine the strengths of formal engines with the strengths of a built-in simulation engine to help engineers uncover deep corner-case bugs in designs.

Hybrid RTL formal verification provides several advantages over traditional RTL formal verification.

• It enables application of formal analysis on large designs. Hybrid RTL formal verification uses formal techniques to drive the built-in simulation engine and reach deep within the design, while continuously performing formal analysis to verify if the design satisfies a given property. This intelligent orchestration of a built-in simulation engine and the formal engines enables hybrid formal verification tools to reveal deep corner-case bugs in large designs.
• It provides deterministic results that are free of false-negative errors. Hybrid RTL formal verification tools ensure that violations detected by formal engines are reproduced in the dynamic verification environment, automatically, starting from a legal initial state of the design. This delivers significant productivity gains because engineers do not have to manually verify all the false-negative violations to find real bugs in the design. False-negatives are also caused by incorrect initialization of formal engines: a formal verification task starting from a state that is unreachable in dynamic simulation results in wasted formal analysis and verification time [Reference IEEE Spectrum, June 2002 "The play in plug-and-play"].
• It enables hierarchical verification by providing support for "assume-guarantee" principle. Assumptions are relationships among input pins of the design. Formal tools use these assumptions as constraints for formal analysis of the design. Hybrid RTL formal verification tools enable reuse of assumptions for one block as assertions for the following block. This reuse guarantees correctness of assumptions used for formal verification of design blocks and hence ensures correct behavior of the design.

The following sections illustrate the highlights of these capabilities in hybrid formal verification tools, such as Synopsys’ Magellan™, which fuses a rich set of advanced formal verification engines with a built-in VCS™ simulation engine.

Verification of Structural Properties
A structural property is a design behavior that can be inferred by analyzing the RTL for the design. Examples of structural properties include the following:

• Full_case and paralled_case synthesis directives
• Out-of-bound array checking
• X-assignments
• Multiple tri-state drivers
• Floating busses
• Register toggle
• Dead code analysis
• Deadlock/livelock conditions
• Clock domain checks
• Unreachable user tasks

Falsification represents a design bug while a proof guarantees correct design behavior for the specified property. When a property is falsified, hybrid formal tools provide a simulation trace illustrating an input sequence that caused falsification. These tools report only those violations that can be reached from a legal state of the design, thus avoiding false-negative errors. They also generate dynamic monitors for properties that are classified as inconclusive: these monitors are reused as assertions in the dynamic verification environment.

Verification of User-Specified Properties
Formal verification of user-specified properties reveals functional bugs in the design. Hybrid RTL formal verification uses simulation engine and multiple formal engines to verify if a design satisfies a given set of properties. To enable this hybrid formal verification, an engineer must create a set of properties that describe the expected behavior of the design and write a set of assumptions describing a sequential or combinational relationship among the inputs to the design. Additionally, a user may need to define an initialization sequence. Hybrid RTL formal verification tools take advantage of the strengths of different built-in formal and simulation engines to reach deep in the design and perform highly effective formal analysis to find deep corner-case design bugs. The orchestration of the use of different engines occurs adaptively and transparently.

Figure 1, below, illustrates the adaptive orchestration that occurs between the formal and the built-in simulation engine in hybrid formal-verification tools.

Figure 1. Adaptive orchestration of built-in simulation and formal engines

The rectangular box represents the entire state space of the design block and the stars represent "promising states," which are design states in the cone of influence of a given assertion. Hybrid RTL formal verification tools, such as Magellan, first play the user-provided initialization sequence in simulation to reach the legal initial state of the design. Then, they perform constrained random simulation (this is represented by the zigzag trajectory) to quickly reach the promising states. From these states, formal engines perform broad analysis to find instances of logic that could violate a given property. This is shown as the concentric circles in figure 1, above. This process of using simulation engine to reach deep in the design and the formal engines to perform broad mathematical analysis from every promising state continues until a property is either proven or falsified for a given set of assumptions. If a property can neither be proven nor be falsified, it is classified as an inconclusive property. The meaning of the three outcomes are explained as follows:

1. Proven. Indicates that the given assertion will never fail for any combination of the input stimuli, as long as the input pin assumptions used to verify the design are valid.
2. Falsified. Represents a scenario (also called counter-example) in which the design violated the given property for the stated assumptions of the inputs. Hybrid RTL formal verification tools always ensure that a bug detected by the formal engines is reproducible in a simulation environment, thus eliminating falsenegative errors.
3. Inconclusive. This could mean that insufficient or misleading assumptions were specified for the inputs of the design, or that the cone of logic influencing the property was too big for the engines to formally prove the property or to find a counter-example. Whatever the reason, inconclusive properties are reused as monitors in the dynamic-verification environment and they can flag violations detected in the simulation environment.

Hybrid RTL formal verification tools use multiple formal engines to be effective on a broad range of design types. Different formal algorithms have different strengths. The hybrid formal verification tools combine the strength of various formal engines with built-in simulation engine. Effective use of the correct engine for a given problem relies on intelligent orchestration of various engines and real-time analysis of the design. For example, Synopsys’ Magellan uses an orchestration algorithm that intelligently activates these different engines according to the topology of the design, the complexity of the property and the status of the ongoing verification task.

Assume-Guarantee and Hierarchical Verification
Figure 2 below shows Block A and Block B connected back to back, as part of a larger design.

Figure 2. Assume-Guarantee Principle

Suppose that the design specifies that consecutive requests generated by Block A must be at least 10 cycles apart. This property can be used as assumption for Block B. While verifying Block B the user "assumes" that the requests coming at the input of B will come at intervals of 10 clock cycles or more. This same property can be used as an assertion for Block A to formally verify if it will ever generate back to back requests that are not at least 10 cycles apart. Thus, assumption made to verify Block B is guaranteed to be correct by using it as an assertion for Block A. This is called assume-guarantee principle and further raises verification productivity.

Hybrid RTL formal verification tools also support hierarchical verification by enabling reuse of block-level assumptions as full chip assertion monitors, used in dynamic verification environment. This methodology ensures that assumptions made at the block-level are held true when various blocks are integrated to create the full chip design.

Figure 3. Hierarchical Verification

Conclusion
Hybrid RTL formal architecture plays a significant role in advancing RTL formal verification. This architecture enables engineers to find deep corner-case bugs, in large designs, early in the verification process. Hybrid RTL formal verification tools, such as Synopsys’ Magellan, cut down verification time and enable creation of high-quality design blocks.

For more information about Synopsys products, support services or training, visit us on the web at www.synopsys.com, contact your local sales representative or call 650.584.5000.