Global Sources
EE Times-India
EE Times-India > EDA/IP

How formal MDV can take out IP integration uncertainty

Posted: 25 Jan 2012     Print Version  Bookmark and Share

Keywords:intellectual property  metric-driven verification  register transfer level 

The combination of formal's exhaustive verification and automatic coverage metric generation delivers much greater IP integration certainty than a slew of iterative dynamic test runs. Moreover, it can be deployed as soon as the first RTL sub-blocks become available, and long before a testbench (even a partial one) has been developed.

How does it work? What factors must be considered? Consider the IP block design-under-verification (DUV) in figure 1.


Figure 1: Factors in the formal verification of an IP block.

Before commencing verification, non-functional code must be excluded from the verification. Modern formal technology automatically identifies and excludes such code, including:

 • Functional code excluded by the constraints (environmental conditions)
 • Unreachable code: code that cannot be verified by any means, formal or otherwise
 • Redundant code: code that implements no DUV function
 • Verification code: code written to assist verification

The formal MDV technology then analyses the remaining "legal" functional code to identify and measure both verified and unverified RTL code—verification holes—to help us to target additional assertions precisely at those holes. We can continue this process until 100 per cent of the RTL has been 100-per cent verified from both control and observation standpoints. And it requires no simulation whatsoever.

Clearly, this application of "quality" assertions—the right assertions in the right places—enhances coverage significantly more reliably and effectively than the assertion density approach.

Moreover, by automatically identifying code excluded by constraints, the technology considerably simplifies the task of detecting over-constraining. And it does so early in the verification, long before the integration stage, where the effects of over-constraining so often surface. Of course with over-constraining we still have the task of determining what the specific problem is. Are the constraints overly restrictive or just plain wrong? Or is the code redundant and can be removed? Clearly, it's much quicker to arrive at a diagnosis without first having to simulate with cover and witness traces.

Using this formal MDV approach, we can say with confidence how thoroughly the IP block's RTL description has been verified, the conditions under which it was it verified, and how accurately those conditions reflect the operating environment into which the IP block will be integrated.

Has the specification been completely implemented?
We can now analyse how thoroughly the RTL design has been verified, but how do we know that we've completely implemented the IP specification to begin with? In other words, how do we know that we've achieved 100-per cent functional verification?

As previously noted, we can do this by constructing a set of operational assertions that expresses intended behaviour—design intent—at the specification level. In other words, they operate at the level of (for example) reads, writes and data transfers, which is also the level of the verification plan. As the set is being built, formal technology analyses all possible input scenarios with their associated output behaviours to identify discontinuities in the set, enabling us to fill the gaps with enhanced or additional assertions. When the set is gap-free and proven against the RTL, the specification has been implemented 100 per cent. Figure 2 illustrates the gap-detection methodology.

Figure 2: Formal analysis identifies assertion set gaps.

The task is to determine whether the DUV—an SDRAM controller—can perform an operation that is not yet covered by an operational assertion. In this case, the set of operational assertions consists of the single_read, single_write, idle (nop) and row_activation operations. The technology finds an input trace, starting after the single_read operation is complete, where none of the existing assertions match. It then generates a counterexample that indicates that there is no operational assertion to cover a burst_write request. We can now write an assertion or modify an existing assertion to fill the gap.

How do we create operational assertions?
The question is now: How do we create operational assertions? Assertion synthesis can't do it; this approach works only with relatively-simple structural assertions at the FSM level in the RTL.

 First Page Previous Page 1 • 2 • 3 • 4 • 5 Next Page Last Page

Comment on "How formal MDV can take out IP integ..."
*  You can enter [0] more charecters.
*Verify code:


Visit Asia Webinars to learn about the latest in technology and get practical design tips.


Go to top             Connect on Facebook      Follow us on Twitter      Follow us on Orkut

Back to Top