How to Reduce the Complexity of Formal Analysis – Part 1 – Finding Where Formal Got Stuck and Some Initial Corrective Steps to Take

When using formal property checking, users often encounter “inconclusive” results; which means that the combined complexity of the design, assertions, and assumptions is beyond the capacity of the tool to compute in one run. In this series of posts we will show how to address this by evaluating the relevant active logic, locating the assumptions and design elements that could cause an inconclusive result, and how to estimate the complexity of the assertions themselves. Then we will discuss methods for reducing the complexity of each of these elements so the analysis will yield a solution.

First-things first: How can you figure out where a formal analysis got stuck?

When a formal run cannot make any progress, the first place to look for root causes is in the “cone of influence” of the logic being analyzed by a given property. Fortunately, today’s formal analysis tools can readily report this information. Plus, Questa PropCheck can also sort the design logic and assumptions used by formal engines according to their importance to the analysis, which helps users zero-in on the most likely sources of trouble. Here is an example:

Starting at the top of the figure, the tool lists “assumptions” and “signals” such that the ones affecting the formal engines the most are on the top. In the bottom half of the screen shot, a summary of the active state bits for registers, counters and memories is also provided. With this information in-hand:

1. Check the assumptions used: generally, removing assumptions can help a lot, especially those that drag in extra design signals other than those specified in the assertion. Paradoxically, sometimes ADDING more assumptions can help too. Of course, recoding an assumption can also bear fruit. These techniques will be addressed in the next post in this series, so bookmark this in your brain for now …
2. Check the signals used: Reducing the complexity of the most significant registers/counters/memories can significantly help an analysis converge. (Again, stay tuned …)
3. Check total state bits: “less is more” when it comes to reaching convergence

If you have an inconclusive formal analysis open in another window, we hope we’ve given you some food for thought to click over to your session and make some forward progress.  In follow-on posts we will elaborate on the techniques we’ve introduced above.

Until then, may your state spaces be shallow, and your analyses be exhaustive!

Jin Hou and Joe Hupcey III
for The Questa Formal Team