Top 10 Tips for Success with Formal Analysis – Part 3

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:

Tip 7: Use formal analysis to improve simulation coverage results by checking for unreachable coverage
Simulation has no concept of unreachability, so it is common for IP and SoC project teams to spend a lot of time and effort trying to hit covers that may be unreachable. Formal analysis can analyze PSL and SVA cover properties and may find that some of them are, in fact, impossible to reach. Combining these results with simulation is very useful since it signals to the verification team that they should stop trying to hit these covers and instead look at why they are unreachable. This analysis may reveal a design bug, such as part of a design being walled off.

In the Cadence® metric-driven verification (MDV) flow, common types of code coverage can be handled by formal analysis as well as simulation. These unreachability results are especially valuable, since most projects rely more on code coverage than PSL/SVA covers for signoff. As with cover properties, verification engineers should not simply toss out unreachable code coverage. Instead, they should analyze each cover to ensure that it really should be unreachable and is not the symptom of a design bug.

A recent Freescale Semiconductor paper described how their verification team used code-coverage unreachability analysis in the Cadence MDV flow to identify coverage that should be “excluded” from the reported results. [1] This allowed the team to achieve coverage closure more quickly and remove the “dead code” after approval by the designer. The Freescale team also used formal analysis to reach coverage that they had not yet hit in simulation.

Tip 8: Use formal analysis to help with coverage convergence by showing how to hit tough coverage
The use of formal analysis for coverage unreachability leads naturally to the question of whether formal techniques can help hit covers that are reachable. In fact, formal analysis can target a cover just as it does an assertion, trying to generate a path from the inputs (within the bounds of the input assumptions) to reach the cover. Many formal tools can target PSL and SVA cover properties directly. Others, as in the Cadence MDV flow, can also target code coverage. In either case, the formal results can be combined with the simulation results.

Verification teams most often think of using formal analysis to try to hit coverage not reached in simulation, generally late in the project. When SoC or IP teams are “spinning their wheels” trying to hit unexercised covers, some of those covers may be unreachable but others may just be hard to reach. Either way, formal analysis can often provide an answer. However, there is no particular reason to wait until late in the project. Some teams use formal analysis to hit coverage early in the project, before a simulation testbench is even available.

There is one important difference between determining coverage unreachability and hitting covers with formal analysis. The latter requires a reasonably complete set of input assumptions since it is not fair to take credit for reaching a cover with an illegal input sequence. Hitting either an assertion or a cover generally requires input assumptions, while proving assertions or determining coverage unreachability is usually done with minimal assumptions. To a formal tool, assertions and covers are very similar in concept.

Just as complex assertions in complex designs cannot always be hit or proven, sometimes formal analysis will neither reach a cover nor prove it unreachable. It is possible that simulation will hit an assertion or a cover that is too complex for formal analysis if it just happens to exercise the right path. In practice, this is not very common except on very large designs that really stretch the capacity limits of formal algorithms. In some cases, the best results can be achieved by using formal analysis and simulation together in an intertwined fashion.