Everything You Wanted to Know About Formal, But Were Too Afraid to Ask

Formal Verification is one of those EDA technologies that’s been used in mainstream development in one or two applications for many years. The true power of the approach only now has started to capture the attention of engineers. Although there are a few reasons for this, perhaps the most significant is formal’s ill-gotten reputation as a mysterious beast too difficult to tame.

After working with formal for almost 20 years, I have lost count of the number of times it’s been suggested to me that you need a Ph.D. to use this tool for full-on design verification. Well, it’s simply not true, especially now. Engineers are smart people (yup, that’s true) and writing assertions isn’t that tough (yup, that’s true, too).

Possibly a more accurate reason might be that formal does appear as a black box that magically tells the user useful information — for example, if certain things can happen. However, it’s not entirely obvious what is actually going on under-the-hood. Engineers like to understand how the black box is figuring out all this useful information. After all, they are engineers. Simulation is easy to understand, formal, less so. Of course, once you have figured out what’s going on, it’s also easier to understand when some garbage in (a bad assertion, say) is resulting in garbage out (bogus results), addressing another concern of the technology.

One way we all like to learn is through case studies, building an understanding what others have done with the technology. Information is out there, but you could spend a week on Google tracking it all down. It’s time we made it easier to find this data. At OneSpin Solutions, we spent several weeks on Google to find the detail and put it all in one place.

Woody Allen plagiarism aside (see headline), it seems fitting that the first blog post on Semiconductor Engineering from OneSpin Solutions should be about FormalWorld.org, an online community dedicated to advancing the widespread use of formal verification.

The goal of FormalWorld.org is to be an open and free online with easy, open access to a broad range of resources to end-users in need of education, information and peer-to-peer networking. Its monthly newsletter will include recent developments and non-commercial, technical postings related to formal verification.

The site is managed by Jan Kuster, an independent consultant. Individuals and organizations are welcome to submit items for posting. OneSpin Solutions provided the initial sponsorship, but we’re taking a hands-off role in its management.

Now I know what you are saying. If OneSpin is behind this, then how can it be unbiased? Well it is. Jan has included any information he could find, regardless of where it came from, whose tool was being used, and what capabilities were highlighted. Why?

Well, the Formal market for design verification (not Equivalency Checking) has been reported at about $80M in revenue (source: EDAC 2014). Simulation revenue is pegged at about 6X of Formal assertion-based verification (ABV), and much greater in terms of license numbers. Given that formal is extremely useful and has the potential to be used across the design flow, then once engineers understand how it can be used, maybe the market will get bigger. As such, should the formal vendors put their effort into competing with each other, or instead invest in making the market larger by helping other people understand these solutions? Clearly, the latter approach is the right one, and this is where OneSpin chooses to place its marketing dollars. We are talking with other vendors, consultants and end-users about how to enlarge and improve the portal.

However, it’s more than just information that is required. Peer-to-peer discussions, questions and answers, ideas from experienced users, are extremely important as well.

A FormalWorld.org blog section is open to the formal engineering community to post non-commercial, technical contributed viewpoints and articles. Visitors will find links to current events and news, a research center with instructional videos and presentations, case studies, academic and topical articles, books and training material, along with a listing of products and service providers. In the future, an independently moderated email questions and answers forum will be available.

Check out the first edition of the site. FormalWorld.org already offers links to a broad range of information sources and will be updated on a continuous basis. The first edition features links to Jim Hogan’s “Guide to Formal Verification,” published in DeepChip.com, a blog post from Gila Logic’s Elchanan Rappaport, and links to videos and presentations from the recent Test & Verification (TVS) Verification Futures.

If you are still asking questions about this technology (and who isn’t?), take a pass at FormalWorld.org. It can be found at: www.FormalWorld.org