What is Formal Design Validation?

Formal design validation is a functional verification methodology that combines aspects of traditional checking and logic simulation based verification methods with the symbolic simulation and static analysis techniques of formal verification. Formal validation combines the ease-of-use methodology and practicality of traditional HDL verification techniques, such as lint and rule checking, with the power of formal verification search technology.

An overview of these design validation methodologies is provided below.

Design Verification Methodologies

Introduction

There has been substantial growth in the market for sophisticated miniaturized electronic products such as cellular phones, notebook and palm computers. These products have been enabled by significant advances in electronic circuit design and manufacturing technology that have made it possible to design and fabricate circuits integrated on a single silicon chip that contain millions of transistors implemented in 0.15 micron ("deep sub-micron") geometry. Electronic design automation software has been an important enabling technology that has helped designers achieve these rapid advances in the design of integrated circuits (ICs) by automating much of the design process, bringing greater efficiency and productivity to electronic design. The design process for complex electronic products typically comprises the following steps:

Architectural or behavioral design,

the design of the system's overall architecture and behavior;

Functional design,

the specification of the design's high-level functionality typically expressed at the register-transfer level (RTL) using a hardware description language (HDL);

Logic design,

the implementation of the functional design into gate level logic, typically performed using logic synthesis EDA software;

Physical design,

the implementation of the logical design into physical components representing transistors and their interconnecting wires performed using placement and routing EDA software.

The vast majority of bugs are introduced during the implementation of the RTL design from the behavioral specification. Currently, model checking is the only available alternative to time-consuming simulation to verify the correctness of the RTL implementation of the circuit,  However, model checking does not actually verify the RTL against the design specification but rather requires the user to first extract a set of design properties from the specification and then attempts to verify that the RTL satisfies these properties.  Thus, model checking requires an experienced user  (it typically takes 3-6 months to learn how to use model checking effectively) who is also very knowledgeable about the design to be verified. In addition, model checking is currently suitable only for small design modules with clearly specified interfaces.

Current Design Verification Methodologies

Design verification is performed after every step of the electronic design process.  The design process typically begins with an architectural design phase in which a behavioral design specification is created either using EDA tools or manually. Behavioral simulation and synthesis tools may also be used during the behavioral design step for some applications (such as digital signal processing). After the behavioral design specification step is performed, the functional design is created at the register transfer level (RTL) using a hardware description language (HDL). After the RTL design stage, design validation is performed to verify that the RTL design is correct. Currently the design validation step is heavily based on logic simulation of user generated tests. After validation, the logic design step is performed, in which the RTL model of the circuit is used as an input to a logic synthesis tool to create a gate level implementation of the circuit. The gate level implementation is again typically verified using logic simulation of user generated tests. However, formal verification is emerging as a way of supplementing implementation verification using traditional logic simulation. Finally, a place and route tool is used to perform the physical design of the transistors and their interconnecting wires.

Current design verification methods span a wide spectrum that ranges from brute-force manual or random test generation techniques to formal verification techniques, such as equivalence checking and model checking, that do not require test generation.

Logic Simulation Based Design Validation Approaches

Logic simulation is the workhorse of today's design validation methodologies. However, despite the increases in simulation speed and computer performance, simulation has not been able to keep up with the rapidly increasing complexity of designs.  For example, a server ranch of  work-stations comprising 1000  processors was required to simulate the 5 billion instruction simulation cycles that were required to verify the Sun UltraSparc I  processor.

An additional issue with simulation based methodologies is that they require the time consuming step of creation of test inputs. Simulators are used to predict the functional response of the design to specified input values. These input values or test vectors are typically generated manually by the designer and provided as input to the logic simulator together with the design description. The simulator's waveform output, which is a prediction of the response of the circuit to the applied inputs, is then compared to the response of the reference model of the circuit (typically created during the previous design stage) to the same inputs to verify that the responses are consistent.

The most commonly used test input generation method relies primarily on manual generation of test vectors. The complexity and laborious nature of manual test generation makes it increasingly impractical as design size increases.

Random Test Generation

The huge search spaces associated with large designs have led to the adoption of random test generation.  This approach typically results in the generation of millions or tens of millions of inefficient test vectors and so results in very long simulation times even when directed or constraint driven random test generation techniques are used. For example, many months of simulation using large "computer farms" consisting of hundreds of engineering workstations are typically required to validate today's microprocessor designs.

Pure random test generation has severe limitations. Despite the large number of patterns generated, the effectiveness in detecting design bugs is limited as typically a large percentage of the tests may not be useful and may violate memory and other environmental constraints. To address the problems associated with pure random test generation, weighting or biasing is generally used to attempt to constrain the test generator to interesting areas of the design space with the intention of trying to cover "corner cases". The problem with this technique is that the design verification engineer may not know or may not be able to determine the direction in which to guide the test generator.

There are two types of random test generation that are commonly used: static, which is carried out prior to a simulation run, and dynamic, which is performed dynamically or "on-the-fly" during simulation.  In static random test generation, the circuit's state is randomly initialized and test sequences are generated. These tests are then verified by simulating them on both the RTL description and a "golden" model of the circuit and comparing the results. Dynamically biased random test generation relies on simulation feedback of the current state of the circuit together with user constraints to determine the next test vector or sequence.

The most commonly used methodologies for large designs today use a mixture of manual test generation and static random test generation. For example on the Power PC 604, the unit test cases were manually generated and random test generation was used during the integrated model test phase. In the latter phase, random combinations of single instructions, enumeration of all pairs of instructions and complex random instruction streams were generated using biasing parameters.

Random test generation techniques are essentially "black-box" techniques that have no knowledge of the internal behavior of the circuit. Deterministic test sequence generation techniques, on the other hand, are considered "white-box" techniques, and rely on knowledge of the function of the circuit. Most deterministic techniques proposed in the technical literature are ad-hoc techniques that typically focus on specific circuit modules such as cache controllers and pipelines. The techniques used are based on state enumeration and traversal and attempt to create input patterns that cause the circuit to traverse each of its possible states and state transitions. The major problem associated with these techniques is that they suffer from the state explosion problem, in which the number of states to be traversed grows exponentially, and so they are not practical for large circuits.

Monitoring Internal Nodes

Because of the very low ratio of system ports to internal nodes, the ability to observe internal logic is typically very low and so is usually increased using monitors and assertions, which are code statements added to the hardware description language (HDL) representation of the circuit. Monitors inspect and display the state of internal nodes, while assertions are "self-checking" monitors that assert the truth of certain properties and display warning or error messages if these properties are violated. The use of monitors and assertions can help boost coverage achieved by the generated tests. However, the construction of assertion checkers and monitors is still generally done manually and is labor intensive. The introduction of application specific assertion checker libraries is beginning to alleviate this problem.

Code Coverage Metrics

One of the major problems in design validation today is determining when the validation process can be terminated. Typically, the main criteria for stopping the verification phase include reaching the cumulative number of simulation cycles targeted and reaching a defect rate of close to zero for a period of a few weeks prior to tape-out. Such traditional criteria do not give a measurable confidence level that all bugs have been detected. As a result, the use of code coverage techniques (borrowed from software testing) are now being used to provide a metric of how good the verification effort has been. Such code coverage techniques rely on statement coverage, variable coverage and branch coverage metrics, path coverage is also claimed but is usually impractical since there can be billions of paths in a design. Code coverage metrics improve the level of confidence in the design functionality compared to previous manual techniques because they identify statements in the RTL description that have not been exercised or variables that have not been accessed. However, they do not prove that design errors have been detected because in addition to exercising a particular part of the circuit it is also necessary to propagate the effects of the design errors to an observable point. Today's code coverage techniques are not able to verify design error propagation.

Lint and Rule Checking

Lint tools, which were first introduced for the C programming language, are now the first line of defense against design errors in HDL representations of designs. HDL lint and rule checking tools, such as Veritable's Design Verity-Check, can statically analyze Verilog and VHDL RTL descriptions and uncover many common design errors such as races, simulation-synthesis mismatches and manufacturing testability issues . According to Harry Foster and Lionel Bening : "A linting strategy targeted as an initial check in the complete line of verification tools is the initial and most cost-effective method of finding design errors ".

Lint tools can also be used to enforce consistent coding styles such as those proposed for design re-use in the Reuse Methodology Manual (RMM) and design for verifiability guidelines such as those proposed by Bening and Foster.

Symbolic Simulation Based Formal Verification Approaches

Formal verification techniques are emerging and are beginning to alleviate the verification problem for certain applications such as verifying the equivalence of two gate level designs. These techniques have the advantage that they do not rely on traditional logic simulation or test vectors and so potentially offer more complete coverage of the design. Instead they utilize integrated symbolic simulators that use symbolic values instead of the logic zero and one values used by traditional logic simulators. The use of symbolic values allows a range of actual logic values to be represented as symbols and so symbolic simulators allow more of the design vector space to be explored than do traditional logic simulators. However, symbolic simulation approaches do not scale well as design complexity increases and are generally difficult to use. In addition, the diagnostic capability when mismatches are found is poor.

There are three basic formal verification technologies that are currently being evaluated by the industry: equivalence checking, model checking and theorem proving. Equivalence checking is used to verify that two structural descriptions are equivalent, model checking is used to verify that design properties are satisfied, while theorem proving verifies that circuits meet their specifications.

Equivalence Checking

The most widely used formal verification technique is equivalence checking, which allows two design implementations to be compared.  Equivalence checking can work well for two structurally similar designs and is often used late in the design process to verify the results of an optimization or test insertion step during logic or test synthesis. However, although equivalence checking can used to verify that a gate level implementation matches the RTL, it is best suited to comparing gate level designs. The technique does not work as well when comparing designs at different levels of abstraction or designs that do not have a one to one mapping of registers, such as designs that have undergone re-timing during synthesis. Equivalence checking verifies that two design implementations are the same; it does not verify that the design is bug-free. In addition, when a difference between design implementations is found, the error diagnosis capability of equivalence checking tools is limited and so it is very difficult to determine the exact cause of the difference.

Model Checking

Model checking uses symbolic simulation techniques to verify that these properties are satisfied for all legal design inputs. In symbolic simulation, symbols are used rather than just logic zero and one values. Temporal logic allows the user to express properties of the circuit over trajectories, bounded length sequences of circuit states. Symbolic model checking is primarily useful in verifying the control parts of a circuit.  It is impractical for most data paths, since it suffers from the state explosion problem where the state space of the design that must be explored grows extremely large. In addition, performing model checking on design modules requires that an interface specification for the module is available so that only legal inputs are considered. However, in practice, detailed interface specifications of design modules are rarely available and so verification often requires the creation of the interface specification. This can be a complex task.

The model checking formal verification approach is heavily dependent on experienced users who must specify the properties of the design that are to be checked. The reliance on a design engineer, who must provide knowledge about design behavior and the design properties to be analyzed, has limited the adoption of this technology. An additional issue is that there is no metric to judge design property coverage and, thus, there is no confidence that all design properties have been verified.

Theorem Proving

Theorem proving involves verifying the truth of mathematical theorems that are postulated about the design using a formal specification language. It remains largely an academic area today and is unlikely to be viable for widespread commercial use in the near future.

Formal Validation

Formal design validation  combines aspects of traditional checking and dynamic simulation based verification with the symbolic simulation and static analysis techniques of formal verification to provide optimized trade-offs in scalability and completeness so improving verification effectiveness. Formal validation checking tools, such as Veritable's Design Verity-Check, extend the ease of use methodology of traditional checking techniques, such as lint, to the area of property checking and so provide a practical and usable alternative to difficult to use formal verification techniques, such as model checking.

For more information on the power of formal validation, please contact us at info@veritable.com.

Please contact our Webmaster with questions or comments.
© Copyright 1998-2003 Veritable Inc.  All rights reserved.