Top 10 Tips for Success with Formal Analysis - Part 3

Thomas L. Anderson and Joseph Hupcey III
EETimes (5/14/2012 9:43 AM EDT)

This article is the final in a series of three offering the “top 10” tips for the successful use of formal analysis on IP and SoC projects. As a reminder, the first and second installments presented the following six tips:

• Tip 1: Involve designers in property specification and, whenever possible, in formal analysis
• Tip 2: Apply formal analysis early in the project so that engineers specifying properties see an immediate payoff
• Tip 3: Leverage all forms of automatic assertions, from basic design checkers through assertion synthesis
• Tip 4: Leverage assertion-based IP (ABVIP) for standard protocols, especially for on-chip buses
• Tip 5: Leverage formal “apps” such as connectivity checking for highly multi-plexed SoC pins
• Tip 6: Recognize the value of formal analysis for both proving assertions and finding design and specification bugs

The previous article closed with a discussion on combining the results from formal analysis and simulation. Since verification leads and project managers are used to assessing progress based on simulation, the most logical approach is to translate formal results into simulation terms. This requires expanding the results reported to include proven assertions. Simulation cannot generate proofs itself but can benefit from proofs from formal analysis. Although not recommended, a user might choose to disable in simulation any assertions formally proven as “safe.”

Shifting from assertions to coverage, unreachable coverage is the corollary to a proven assertion. When formal analysis proves an assertion, it mathematically determines that there is no legal path from the inputs (within the bounds of the input assumptions) that can violate the assertion. Similarly, an unreachable cover is one for which there is no path from the inputs that can reach the cover. The main difference is that unreachability analysis can be performed with few if any input assumptions; if a cover is unreachable with no assumptions, it is also unreachable with them. This leads to the following tip:

Click here to read more ...