Achieving completeness in IP functional verification

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.

Click here to read more ...