Tip 9: Recognize the value of “dual-engine” formal analysis and simulation working together on assertions and coverage
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
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
recent NVIDIA paper discussed the use of assertion-driven simulation on
a complex, multi-stage memory controller.  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
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.
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.
“Innovative Approach to Coverage Closure Through Un-Reachability
Analysis Flow” by Ashish Goel, Tejbal Prasad, and Abhinav Nawal,
CDNLive! India 2011,
“IP Verification Methodology Using Property-Driven Simulation in
Incisive Enterprise Verifier” by Deepanjan Roy, Abhishek Datta, and
Lokesh Babu Pundreeka, CDNLive! India 2011,
Thomas L. Anderson, is a technical marketing consultant who recently served as Product Management Group Director for Cadence.
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]).