Is This The Era Of Automatic Formal Checks For Verification?

I was thinking about the above question and recalled something IBM would repeat annually back in the late 1980s about its OS/2 replacement for MS-DOS. “This is the year of OS/2!” they would shout. But the marketplace wasn’t listening. As one buddy of mine liked to say, it was only half of an operating system (O.S./2).

In the last nine months, my company, Real Intent, along with our competitors in the EDA market have been making announcements about their respective RTL verification tools that employ automatic formal engines to solve specific design issues.

Wally Rhines, CEO of Mentor Graphics in his keynote speech at DesignCon 2013 this week in San Jose made this very same point in his presentation:

“Originally formal property verification was tough to use, and required a Ph.D. and a very sophisticated designer. There was formal property checking done at companies but it was pretty specialized. And what happened in the last decade is people identified specific tasks that were narrow enough that you could develop formal methods that would automate that portion of the verification [task] and more and more people innovatively found different things you could check. So that today, fully automatic formal is a reality for a lot of companies. And is what I would call in many cases push-button formal. You don’t have to be an expert. You basically get the tool, load the data, and press a button and you get a result that is useful and useable. If this doesn’t happen, we would have a real problem out in time doing all the verification we have to do. And there are some things that really can’t be effectively verified without formal methods.

“If we look at our survey data…the larger the design, then more formal is used. 41% of designs over 20M gates [in size] are using formal verification of some sort. And If I look just across the industry, so what things are available today in push button form that you can actually use easily? A bunch of things come to mind…”

Wally then highlighted how clock domain crossing (CDC) analysis now takes advantage of formals methods for full-chip verification, and then went on to show how finding dead code and eliminating it with an automatic formal tool improves code coverage metrics for a design project. Similarly, he mentioned how a problem in a base architecture which used an FSM with an unreachable state could also be easily identified, or analyzing how ‘Xs’ (unknowns) are propagated in the design which is a common reset issue that needs to be verified.

Wally’s final slide concluded that with the acceleration of innovation in design, some of the macro enablers for verification success are multi-engine verification platforms and application-specific formal. With 41% of designs over 20M gates using formal verification; I think the era of automatic checks has definitely arrived.