Happy Birthday, Decoding Formal!

On the radio yesterday, we heard that the song “Happy Birthday To You”, one of the most widely sung tunes in the world, was ruled by federal judge George H. King to finally be in the public domain!

This welcome news seems to come at the right time, as Oski Technology plans to celebrate the second anniversary of the Decoding Formal Club at our quarterly meeting on October 21 at Computer History Museum, in Mountain View.

Since it was founded in October 2013, the Decoding Formal Club has drawn the attention of engineers, designers and verification managers. In a relatively short time we have covered much ground, and become a forum where formal knowledge and experience can be shared among the growing community of formal enthusiasts. In turn, Oski’s featured presentations have covered many aspects of formal sign-off methodology: Bounded Proof, Abstraction Models, Formal Test Planning, End-to-End Checkers and Constraint Management.

While survey comments from attendees indicate that Decoding Formal meetings are enjoyable and worthwhile, the numbers provide hard evidence that these events have garnered quite a following: Attendance at Decoding Formal events has increased 4x since its inception. We regularly receive requests to bring Decoding Formal events to more cities, and attendees fly in from out of state, to attend our events.  This demonstrates not only the success of our Decoding Formal events, but also the increasing and widespread interest in the adoption of formal verification, in the industry.

Our aim was to create a forum for the advanced application of formal verification, as well as offer lunchtime networking with peers, and the chance to explore the unique collection at the Computer History Museum, including the historic Babbage Engine. The Decoding Formal Club has largely achieved this objective, but not without lively (and sometimes heated) technical discussion. We are grateful to formal users who attend and share their experiences and challenges at these meetings, as well the many industry-leading formal experts who have presented valuable insights gleaned from their day-to-day practical application of formal verification:

• Vikram Khosa, “One Metric to Rule Them All: Tracking Progress on Formal Testbenches”
• Robert Kurshan, “Formal Verification of Cache Coherence”
• Jonathan Michelson, “Liveness vs. Safety – A Practical Viewpoint”
• Normando Montecillo, “Can Formal Go Mainstream? Broadcom DVT’s Formal Integration in the DV Flow”
• Syed Suhaib, “Experience with Formally Verifying the Denver CPU”
• Ross Weber, “Formal Verification and a New CPU Project at ARM”

At the upcoming meeting on October 21, we are pleased to present the following speakers:

1. Prashant Aggarwal, project lead and principal engineer at Oski, will present “How to Ensure Completeness of End-to-End Formal Testbench for Sign-off”
2. Kenny Xing, principal design engineer at Broadcom, will share “Creative Formal Techniques to Verify PCache”
3. Yogesh Mahajan, verification engineer at NVIDIA and Vigyan Singhal, Oski CEO, will discuss “Compositional Reasoning Gotchas in Practice”

In addition, we are delighted to have Vikas Chandra, Principal Engineer at ARM who will talk about Mobile Hardware Security.

Lastly, if you’ve seen the new video of our popular “Break the Testbench” Challenge* at this year’s DAC, you will have seen formal in action. This is something we are regularly asked to incorporate at Decoding Formal, so for this meeting, we will be bringing the challenge to you. You will be able to examine the end-to-end formal testbench, insert functional bugs, debug counter examples to verify the failure was triggered by the bug, and prove for yourself that the bug you inserted, was in fact caught.

So please join us on October 21. There will be a large cake, and a small birthday celebration for Decoding Formal. We are happy to report that space is truly limited, so sign up today.

*The October 21 Decoding Formal Club meeting is sponsored by Synopsys. The “Break the Testbench” challenge is supported by Synopsys VC Formal.

Tags: "Decoding Formal" Club, #ARM, formal analysis, formal verification methodology, Oski "Break the Testbench" Challenge 2015 DAC, Oski Technology, Oski Verification Challenge, Prashant Aggarwal, Vigyan Singhal

Category: Blog

This entry was posted on Thursday, September 24th, 2015 at 2:04 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.