Top 10 Tips for Success with Formal Analysis – Part 3

Tip 9: Recognize the value of “dual-engine” formal analysis and simulation working together on assertions and coverage
The most common “dual-engine” technique is using simulation to set up an interesting starting point for formal analysis, rather than starting at reset. Some formal tools can read in a trace file from simulation and initialize to a state reached in the simulation run before starting analysis. The canonical example of this is a design with a deep FIFO and a “FIFO full” cover. Capacity limitations may prevent formal analysis from generating a path from reset that fills up the FIFO and hits the cover.
Running a simulation that fills up most of the FIFO and starting formal analysis at that point may be more successful. This technique is especially interesting for assertions related to the “FIFO full” condition, for example that the FIFO should never overflow (i.e., accept a write when already full) and lose data. Note that starting from a non-reset state is usually not valid for proving an assertion or determining an unreachable cover, since these require analysis of all possible behavior after reset.
The Cadence MDV flow provides additional forms of “dual-engine” operation that can be helpful in reaching assertions and covers that are hard to reach with simulation or formal analysis alone. The most valuable of these is assertion-driven simulation, in which the same input assumptions used for formal analysis are also used to generate simulation stimulus. If the resulting path running in simulation hits an assertion or a cover, the user knows that this is valid since only legal input stimulus (within the bounds of the input assumptions) were applied.

Assertion-driven simulation opens up new verification possibilities, especially for designers who can:

• Run simulations on their block before any testbench is available
• Discover early bugs whenever assertions are violated
• Find proven assertions and unreachable covers
• Refine the input assumptions based on the paths generated
• Learn about an unfamiliar block reused from another project

A recent NVIDIA paper discussed the use of assertion-driven simulation on a complex, multi-stage memory controller. [2] This unique technology allowed the NVIDIA team to develop appropriate input assumptions for the design, identify the “sweet spots” for formal analysis, and find interesting design bugs early in the development process. Perhaps the most interesting bug found was a case in which a client was granted memory access without even requesting it.

Tip 10: Use formal analysis to track down the source of post-silicon bugs whose effects can be captured with assertions
Although formal analysis is usually used for pre-silicon verification, it also plays a very valuable role for certain kinds of bugs found in the lab. The effects of a hardware bug may be seen at the system level, such as when a program crashes. If the bring-up engineers can narrow down the bug effects to an incorrect behavior that can be described with an assertion, then formal analysis can be run to find a path that could violate the assertion. This approach can save days or weeks in the lab trying to use a logic analyzer to find the source of a post-silicon bug.

This series of articles has presented 10 tips for increased success with formal analysis. Some may be obvious to the experienced formal analysis user, but not to the novice. By following these rules, both new and current users can obtain better results from their tools, leveraging their investment and while gaining the certainty and completeness that only formal analysis can provide. Any comments or suggestions for additional tips are welcome. There is a lot of successful formal use in the industry, and sharing best practices can benefit everyone.

References
[1] “Innovative Approach to Coverage Closure Through Un-Reachability Analysis Flow” by Ashish Goel, Tejbal Prasad, and Abhinav Nawal, CDNLive! India 2011, http://www.cadence.com/cdnlive/in/2011/pages/proceedingssummary.aspx
 
[2] “IP Verification Methodology Using Property-Driven Simulation in Incisive Enterprise Verifier” by Deepanjan Roy, Abhishek Datta, and Lokesh Babu Pundreeka, CDNLive! India 2011, http://www.cadence.com/cdnlive/in/2011/pages/proceedingssummary.aspx

Thomas L. Anderson, is a technical marketing consultant who recently served as Product Management Group Director for Cadence.
Joseph Hupcey III, Product Management Director, Advanced Verification Systems, Cadence Design Systems, Inc.

---

If you found this article to be of interest, visit EDA Designline where you will find the latest and greatest design, technology, product, and news articles with regard to all aspects of Electronic Design Automation (EDA).

Also, you can obtain a highlights update delivered directly to your inbox by signing up for the EDA Designline weekly newsletter – just Click Here to request this newsletter using the Manage Newsletters tab (if you aren't already a member you'll be asked to register, but it's free and painless so don't let that stop you [grin]).