“What if” All Design and Verification Engineers Used Formal?

What if all design and verification engineers used formal? What if formal tools become smart enough to do the abstractions? What if formal tools had infinite capacity? These and other questions were proposed by attendees on the event survey for this quarter’s Decoding Formal Club event on October 23, 2014 at the Computer History Museum in Mountain View, CA. Plenty of first time attendees were there, testament to a growing interest in exploring the possibilities of formal verification. As a formal verification services company, this is very exciting for us, and a good sign that the Decoding Formal Club forum is helping to build critical mass for serious discussion of the application of formal verification in the industry.

An increasing number of people are indeed becoming interested in formal. The Decoding Formal Club was founded in 2013, and this, our fourth meeting, was the best ever attended event with over 45 participants; for the first time we had to turn people away. Attendees came from companies including Apple, NVIDIA, Broadcom, Qualcomm, Palo Alto Networks, Ericsson, Marvell, XPliant and Google, and with varying levels of expertise and familiarity with formal verification. Some are new to formal, others have years of experience. Many companies are seriously invested in the idea of adding formal to their verification flow.

The formal adoption curve is growing exponentially. Part of the draw of our recent Decoding Formal Club event was the program of talks including those by two new speakers, Robert Kurshan, a pioneer in formal verification, and Syed Suhaib, formal manager at NVIDIA, who talked about his real-world experience formally verifying the NVIDIA Denver CPU.

As Kurshan pointed out in his talk, this is an extremely exciting time to be working in formal verification. The last few years has seen a surge of projects and focus in formal verification. The work that academics have been doing is finally reaching what he called critical mass. Customers want more and more, faster and faster. We now have user-guided formal verification that is spurring the industry to do better and better. It is no longer a question of when. We are here.

The overall response of attendees to this message was extremely positive. Engineers who are starting to successfully apply formal understand that if you are willing to think laterally and solve problems, can focus on formal verification and apply it again and again, you can become effective with it.

Moreover, the general feedback on the event was very positive. The presentations ranged from introductory-level to advanced, and were designed to target a wide audience including project managers, as well as engineers who work with formal on a daily basis, and most attendees described the presentations as “excellent”, and rated the topics as important and appropriate. In general, attendees agreed the content was very informative, useful, practical, and was immediately applicable to current issues. Some surveys suggested the presenters cover more examples, tips and practices. Others requested future events cover more on the test planning process, metrics, coverage, modeling, more case studies and detailed examples of how formal was used, as well as the criteria for a successful formal project as compared to formal projects that fail. These and many other topics were suggested, enough to provide discussion for many future Decoding Formal events.

Our giveaway for this event was the recently published “what if” book by Randall Munroe, now on the New York Times best seller list. We asked attendees to pose their own “what if” questions as a way to announce our theme for the next Decoding Formal event in January 2015, and provide user-guided direction for discussion topics.

Our “what if” survey question provoked some other lively and controversial questions on a range of interesting topics, many of which were about formal verification. All the questions were thought provoking and insightful. What if all design and verification engineers used formal? What if all engineers used formal for sign off?. What if formal verification could run on machines with infinite processing power?

These “what if” questions pose exciting problems which we will discuss at the next Decoding Formal Club event in 2015. Formal adoption is on a strong upward trend. People are really interested in and excited about what is possible with formal. Two attendees asked “what if” formal completely replaces simulation? Another asked “what if” the attendees for the Decoding Formal Club doubles? We are betting on it. We hope you can join us in January 2015, date to be announced.

Subscribe to our mailing list today to receive notification of upcoming Decoding Formal Club events and news about Oski Technology. General information about the Decoding Formal Club, is here. To view video and agenda for past events, visit the Decoding Formal tab at www.oskitechnology.com.

Tags: "Decoding Formal" Club, Apple, Broadcom, formal sign-off, formal verification methodology, NVIDIA, Oski Technology, Palo Alto Networks, Qualcomm, Robert Kurshan, Syed Suhaib, Vigyan Singhal

Category: Blog

This entry was posted on Monday, November 10th, 2014 at 6:28 am. 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.