In a fascinating (to me) twist of fate, I will be moderating a panel on the “next big thing” in formal methods at FMCAD 2009 in Austin, Texas. The panel, entitled “What will be the next breakthrough solutions in formal?” is being held from 11:50-14:00 on Wednesday, November 18, and is made up of four distinguished panelists:
- Harry Foster, Mentor Graphics
- Ziyad Hanna, Jasper Design Automation
- Kevin Harer, Synopsys
- Axel Scherer, Cadence
Those of you who have been reading Cool Verification for awhile will note that I have never really discussed the topic of formal methods on this blog. Truth is, I’ve yet to come across a situation on a project where I needed to use formal to get the job done. My theory is that there are a couple of issues preventing wide-spread adoption of formal tools in a standard verification flow. First, the impression I get is that using formal well requires special expertise to write appropriate properties, partition the design, and interpret the results of the tools. Second, the fact that you need special tools at all. In other words, the fact that I need a separate tool in my flow other than Questasim, VCS, or IUS (not to mention a separate license) makes it difficult for someone to try out formal techniques outside the tool flow of a typical project.
During the panel I plan to ask panelists about just such issues, plus several other questions proposed by thoughtful engineers just like you on the Google Moderator site set up for just this purpose. In fact, I’d like to request your assistance. If you have a question you’d like to see asked of one of the panelists please submit it (or vote on your favorites) via the Google Moderator site or by mailing me directly at jl at coolverification dot com.
I’m also quite interested to hear any stories readers may have with respect to the adoption (or lack thereof) of formal tools in your respective companies and current projects. There are several types of formal tools out there… Any types of tools you’ve had great success with in particular? Or great failures? Does the choice of formal technique heavily depend on the application domain in question? What do you think the EDA vendors need to address in tool functionality/usability in order for you to consider adopting formal more broadly?
And of course, if you’re planning on being in Austin for FMCAD please let me know!
