Guest Post: Yes, Formal Will Dominate Verification

As I hoped, my recent post challenging Jasper Design Automation’s statement that “formal will dominate verification” has drawn very good readership and generated some stimulating industry discussions. Today, Joe Hupcey III from Jasper responds and offers more ammunition for their claims of dramatic recent advances in the power and usability of formal technology:

Thanks to the folks at Breker for the comments and analysis in your post asking “Will Formal Really Dominate Verification?” in reference to Jasper’s recent assertion of formal’s ascendancy. As your thoughtful post acknowledges, verifiers are seeing formal starting to take over block and unit level verification, as well as select system-level applications. Indeed, the industry has seen this movie twice before – specifically, the growth of emulation into the mainstream and again with constrained-random simulation.

Today, Jasper sees the signs of a market that is not turning back given the big productivity and quality gains our customers are experiencing. For example, at our October users group meeting the presenters reported finding 10%, 25%, even 40% of the total bugs on a project using Jasper – at greater than 2x the engineering productivity compared to simulation, and a general goal of replacing simulation with formal in unit-level verification in the near term.

The mainstream market can’t ignore results like this, and must realize that there are big productivity and quality gains available with new formal methodologies. As such, companies will begin tuning their design styles, flows, and even their engineering teams to accommodate formal in order to capitalize on the productivity and quality improvements. Suffice to say, we are seeing this acceleration happening in Jasper’s customer base.

Clearly, the remaining points of contention are around whether formal technology can scale to support true end-to-end verification of system level behaviors that require analysis of the full design. Allow me to share with you some more data that suggests formal is trending in this direction faster than is commonly believed:

• Echoing the examples in the original post, it bears repeating that for block and unit level verification customers are realizing that it’s not worth the months of cobbling together and debugging a UVM testbench (which, at best, will only be reused as a monitor at the system level) when, with a few assertions (either manually written or generated by a formal app like Behavioral Property Synthesis), Jasper Formal can handle verification of the whole enchilada. There are plenty more cases of Jasper Formal “encroaching” on what was once the exclusive domain of simulation in the areas of low power verification, X-propagation analysis, security path verification, and more.
• Looking inward to our R&D development trends, we are seeing our engine capacity – both individual engines and the collective throughput of our multi-engine, multi-core ProofGrid – scaling much faster than Moore’s Law. If this trend continues, formal is bound to “catch up” with simulation scalability. When the trend lines will cross is unclear, but remember how people never believed RTL would replace gate level, or that constrained-random generation would ever replace carefully crafted directed tests?
• Finally, this whole initiative isn’t about simply replacing simulation with formal on a 1-for-1 basis, i.e,. pretending formal analysis of assertions is a clever replication of directed or constrained-random tests. Instead, it behooves customers to take advantage of how formal can approach verification problems differently. For example, recall the comment in the Breker post that “Dynamic power analysis, in which switching activity is measured for long emulation runs, has no formal equivalent.” In fact, with formal employing new “noisy trace” technology (the opposite of our “quiet trace” algorithms) together with behavioral property synthesis, customers can fulfill this same verification need. Another example is the infamous sequential fault-grading problem that test people have been chasing for years. A customer approached us about this, and we were able to delight them by quickly developing a formal-based solution.

Add it all up, and the proliferation and successes of formal apps and methodologies we see in our current customer base, in addition to the relatively sudden emergence of a host of new prospects, all give credence to Kathryn’s/Jasper’s thesis.

But how steep is the slope of this trend line? Kathryn herself cautioned that the time horizon for eventual ‘domination’ could be many years in the future depending on the given verification task(s). Indeed, she stated that formal will never replace all simulation – it’s just that simulation will eventually become the niche product, well suited for special tasks. But as noted above, the adoption and scalability curves are both bending upward. Again, our engine scalability appears to be significantly outpacing Moore’s Law. And in parallel we continue to invest in lowering the adoption barriers for formal novices (with more automation of assertion generation, innovative GUI setup and debug workflows, new formal “apps”, etc.) So while “it’s tough to make predictions, especially about the future”, formal replacing most (but not all) of simulation is inevitable and the momentum is unstoppable.

Thanks again for the original post and the opportunity to respond!

Joe Hupcey III
Jasper Design Automation

Tags: Breker, constrained-random, EDA, formal analysis, formal apps, jasper, Moore's Law, simulation, SoC verification, uvm

This entry was posted on Wednesday, December 4th, 2013 at 12:08 am. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.