This article formalizes the concept of best possible verification quality -- completeness -- and describes a methodology, field-proven on many complex module and intellectual property (IP) designs, that tells you when verification is complete. To demonstrate the results, it summarizes the verification of a protocol processor IP from Infineon.
How do you know when functional verification of IP is complete? Functional verification is complete when the IP's implemented behavior and specified behavior correspond with each other. At this point, the design is error-free.
But how do you know when that is? Is it when every line item in the verification plan is checked off? Is it when 100% of the RTL code is covered? Or is it when last week's verification runs have detected no further errors? And does achieving these "completeness" goals imply that the design is free of functional errors?
No. These "completeness" definitions are relative metrics that track verification progress and "guesstimate" achieved verification quality. Generally, they do not ensure that the design and specification are error-free.
"Completeness" is an absolute concept, not a relative one, so it needs an absolute, and tool-independent, definition: verification is complete when every possible input scenario has been applied to the design under verification (DUV), and every possible output signal has been shown to have its intended value at every point in time.
Does this mean you must adopt a special design-for-verification methodology? Or, does it mean you must re-implement the existing design in your verification environment? And is this definition at all practical in a world of limited resources? After all, a pipelined processor, for example, has trillions of trillions of different circuit states. However, simulation-based verification executes at only a tiny fraction of real-time circuit operation speed. Consequently, simulation mandates a trade-off between verification coverage and verification resources that argues against the very concept of completeness. Moreover, in the case of IP, simulation-based verification does not adequately define the hardware/software environment(s) into which the IP can be easily and reliably integrated " a serious impediment to IP re-use.
Generally speaking, formal verification has similar problems. Single properties are exhaustively proven with respect to all possible input scenarios. However, the properties typically have an implicative structure: for a specific input pattern (for example, a write request is received by a bus arbiter), the property makes statements about the resulting DUV state and output behavior (for example, the arbiter transmits an acknowledgement). Consequently, a single property typically verifies only a fraction of the possible input scenarios and their associated output behaviors. Therefore, a set of properties must be developed to capture the DUV's entire behavior. This leads immediately to the central questions in formal verification: "Have I written enough properties, or are there gaps in the property set? Is every possible input scenario inspected and is its effect on the states and outputs verified by at least one property?"
Consequently, this concept of "completeness" leads to a new definition of quality for formal verification " the property set must be gap-free. Combined with the exhaustive verification of single properties, a gap-free property set ensures the most rigorous verification possible. Historically, however, no formal verification methodology has been able to address the issues of how to identify gaps in property sets analytically and automatically, and how to provide the necessary diagnosis information to systematically close these gaps by writing additional properties. And none have adequately addressed the integration environment issue. Can these problems be solved?
Yes, but before answering "how?", it's important to address the issue of completeness and its implications in greater depth.
Completeness and its implications
Design verification is really design/specification co-verification. The module or IP design is verified against the specification while, simultaneously, errors and omissions in the specification are (hopefully) detected and corrected.
An implementation error that escapes verification and ends up in the final chip is generally one of three types: unstimulated, overlooked, or falsely accepted errors. An unstimulated error is one in which the input stimuli fail to trigger the error, and propagate its effects to the outputs; an overlooked error is one in which the error is triggered, but there is no monitor or property to observe and flag the erroneous behavior; and a falsely-accepted error is one in which erroneous behavior at the outputs is not detected because both the RTL implementation and the monitors or properties deviate in the same way from the specified behavior. Of course, the specification itself may be incomplete or incorrect, and thus not reflect the originally intended behavior.
Clearly, a methodology for complete verification must detect these errors reliably and consistently. Therefore, verification coverage is a combination of:
- Input scenario coverage: the ability to avoid unstimulated errors;
- Output behavior coverage: the ability to avoid overlooked errors; and
- Specification compliance: the ability to avoid falsely accepted errors.
Approaches including testbench reviews, property reviews and executable specifications are used to address specification compliance. Established coverage metrics, and the tools that produce them, address the input and output coverage dimensions. However, they leave much behavior unexplored, and thus fail to achieve completeness.
Inevitably, the question arises in all verification projects: "How much coverage do you have?" Richard Goering of EE Times poses the question another way: "Let's say you get a metric that says you've achieved 98.6 percent verification coverage on a given intellectual property (IP) block. What does that really mean?"
The issue underlying these questions is "What behavior, intended or unintended, have you not covered, and how can you close this gap?" One formal verification methodology exists today that efficiently produces a "complete" --or "gap-free" -- property set; it achieves 100% input scenario coverage, 100% output behavior coverage, and evaluates specification compliance analytically. This methodology:
- Requires no design-for-verification methodology
- Requires no recording and analysis of other coverage metrics, such as code coverage, functional coverage, transaction coverage, finite state machine (FSM) coverage, toggle coverage, fault-injection coverage, etc.
- Eliminates the need to anticipate corner case scenarios in advance, because complete verification covers all corner cases, anticipated or not.
- Detects and analyzes previously unknown, and thus uncovered, behavior without time-consuming manual labor.
- Systematically detects specification errors and omissions, because a property error or gap often reveals a specification error or gap.
1. Verification coverage vs. duration and effort curves vary various methodologies
Comprehending well-defined requirements for integration into the target hardware/software environment(s), engineers can integrate the module or IP into the chip. Coverage-driven chip-level simulations then can be performed with confidence that the modules and IP are error-free, thus eliminating the late error detection that threatens tape-out deadlines.
This IP verification completeness corresponds to full equivalence between a property set and an implementation, and results in both a corrected specification and a complete, specification-compliant set of exhaustively proven properties. In other words, completeness achieves true functional sign-off. How is it possible to achieve this verification completeness?
|
