April 21, 2014: A-Day for Formal Analysis

Yesterday may well go down in EDA history as one of the most important days in the evolution of the market for formal analysis. If you had asked me why yesterday morning, I would have said it was because I was attending the third “Decoding Formal Club” meeting sponsored by formal consulting experts Oski Technology. The range of companies represented there, and the enthusiasm for the topic, was a clear indication that formal has become an A-list technology for many verification teams.

So I planned to write today’s post about this meeting. But then, just as it was ending and Oski was thanking all the participants, news broke that Cadence had acquired formal leader Jasper Design Automation for $170M. Of course, this news was of intense interest to the attendees. It made yesterday “Acquisition Day” for formal analysis, so I’ll dub it “A-Day” and provide some thoughts in this post. I will talk a bit about the meeting as well, but will go into more details about the material presented in a future post.

As regular readers know, I spent more than ten years involved in applications engineering and marketing for formal products at 0-In Design Automation (now part of Mentor Graphics), Synopsys, and Cadence. I’ve also consulted at various times for several other companies with products based on formal techniques. I still have a soft spot for the technology, and have blogged before on the differences and similarities I see in the evolution of SoC verification and formal analysis.

I can’t help but regard the acquisition of Jasper for $150M+ as a major endorsement of the importance of formal in today’s verification arena. Note that Cadence already had a very talented team of engineers and successful formal products, so they had invested a lot in this area already. Adding Jasper’s products to the mix represents even more commitment and investment to formal technology. Cadence will be the undisputed formal market leader with its combined solutions.

In fairness, this is not the first time that a major EDA vendor has made such a statement. In 2003, Cadence acquired Verplex, who had formal analysis (BlackTie) in addition to their better-known family of equivalency checkers (Conformal). Almost exactly a year later, Mentor Graphics acquired 0-In. Although terms of these acquisitions were never publicly disclosed, it seems likely that neither valued formal analysis as highly as does the Cadence-Jasper deal.

In my years pitching formal tools, there were times that I wondered whether they would ever become mainstream. It was a long path to get formal analysis from “nice to have” to “must have” for verification teams. It’s a rare company that is not using formal at some level today, at least “under the hood” for checking SoC connectivity, clock-domain crossings, power domain control, and other applications. Many are also specifying or generating assertions and using formal analysis to either prove them correct or find RTL bugs.

These same themes were echoed in yesterday’s Decoding Formal Club meeting. Formal applications are a given for the companies and project teams represented there, with most also using assertion-based verification at some level. Some teams are dispensing with simulation entirely for certain types of block-level designs. This “end-to-end” formal approach is one of Oski’s specialties and I will talk more about it when I post the details of the meeting.

I am pleased at how far formal technology has come in the past fifteen years. We pioneers did get pierced by plenty of arrows, but the wounds have healed by now. I’m truly excited to be a pioneer again in the SoC verification market. I believe that we can revolutionize full-system verification as completely as formal analysis transformed block-level verification and formal applications automated many types of chip-level checks. I look to the success of Jasper as a good model for Breker and other EDA companies pioneering new approaches.

Tom A.

The truth is out there … sometimes it’s in a blog.

Please visit us today at www.brekersystems.com

Tags: 0-In Design Automation, Breker, Cadence, EDA, equivalence checking, formal analysis, functional verification, jasper, mentor, simulation, SoC verification, Synopsys, Verplex

This entry was posted on Tuesday, April 22nd, 2014 at 5:55 pm. 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.