Shortly after DAC 2010, Gabe Morretti wrote a couple of interesting blogs (reference links below) on how associating the name "verification" with formal was a bit of a misnomer. (Just to be clear, Gabe was referring to formal property verification (FPV) and not formal equivalence verification.) He feels the label should be "Formal Design" and justifies this by the fact that assertions need to be developed simultaneously with the RTL. He also goes on to suggest that the lack of financial success of any vendor in this space is due to "erroneous positioning of the tools" toward verification specialists and not towards designers. I took issue with some of Gabe's assertions (no pun intended) at the time, but couldn't find time to respond until now. Here goes....
While I agree with Gabe that designers should be integral in using assertions and formal, I would argue that formal tools have been properly positioned. Case in point: looking back at the release of Incisive Formal Verifier ("IFV") in 2004, our team was the first to develop and focus a methodology specifically targeting designer productivity -- expediting all bring-up processes that occur before a testbench even exists, as performed by RTL designers -- not verification engineers. We still invest heavily in this use model because we continue to see many customers getting the most bang for the buck for formal adoption this way. Our competitors appear to feel the same way, since we've been flattered by their re-engineering of their tools and methodologies to also be a player in the designer space over the last few years. So I don't think positioning in-and-of-itself has been a constraint on economic growth.
The truth is that Cadence has made significant headway with designers who are new to formal, but I also won't argue that we wouldn't like to see greater adoption by the design community. The question, then, is if the tools are positioned properly, why the lag in adoption by designers? Perhaps it's the economy, and with "right-sized" teams there's just no time or money to invest in anything "new." I've also met several prospects that still consider Formal Property Verification (FPV) a luxury item that's not required for tape out. Of course, anyone who has seen the power of formal analysis first hand would disagree, but such bias is still out there. Or maybe the industry has limited mindshare in general, which over the last few years has been dominated by advanced testbench methodologies (and associated battles). With so much buzz on OVM, VMM and UVM how could anyone avoid being pulled into the debate? Even as a formal guy I couldn't avoid the mayhem!
While it's hard to predict the exact reasoning, in the last few years there certainly has been an interesting development in formal adoption and growth (ironically predicted by EDA360's "Silicon Realization" concept) that has recently started to snowball in popularity: SoC integration verification. The FPV SoC integration solution offered by Cadence was co-developed with Freescale and presented at CDNLive! San Jose in 2006. Since that presentation was given 4 years ago, the "SoC Connectivity" flow with IFV has steadily spread to over 25 unique companies with multiple sites. Hence, along with continuous improvements in designer verification flows, we are also investing heavily in this space. Back to Gabe's point: maybe the label should be "formal integration?" Likely not.
If there's anything I have learned in my years working in the formal space, it is that we should not pigeon-hole the technology. Our customers challenge us every day to apply it on new and interesting problems. With the economy hopefully recovering, UVM leveling the playing field in the advanced testbench space, and Cadence's continued investment in formal, hopefully people will have the opportunity to invest in formal and see the benefits many are taking advantage of today. Hence, if anything the term "Formal" should stand alone, or be used a prefix for the evolving and completely novel applications that are increasing the size of the EDA market as a whole.
Chris KomarTeam Verify Solutions Architect
On Twitter: @teamverify -- http://twitter.com/teamverify
Reference LinksGabe on EDA: Formal Verification: An Unfortunate Labelhttp://www.gabeoneda.com/news/formal-verification-unfortunate-label
Gabe on EDA: Formal Verification: An Unfortunate Label - The Sequelhttp://www.gabeoneda.com/news/formal-verification-unfortunate-label-sequel