A Formally Free Lunch

I am sure many of you can remember the successful events staged by Eric Hennenhofer, founder and CEO of Obsidian Software. While neither his name nor that of his company may be on the tip of your tongue, DVClub might ring a few more bells. He started it so that he could have a place to meet fellow engineers while enjoying a free lunch. It grew very rapidly and with the help of a number of sponsors, regular events were held in Austin, Boston, Silicon Valley and spread throughout the world. In 2011, Obsidian was acquired by ARM, and the events almost faded into obscurity. Today, they do still happen but tend to be quite sporadic, organized by local people.

Recently, another such learning opportunity has come about. This one is also in the verification space, but focusing on . Decoding Formal was started in 2013 by Oski Technology, a services company in the formal verification space, and Decoding Formal meets every 3 or 4 months. The last of these events was held in the Computer History Museum in Mountain View and the room was packed. Synopsyshas recently stepped up to sponsor the event.

Three talks were given, each very different. , the CEO of Oski gave the first talk and discussed a couple of techniques that could be used to decrease the size of the reference model that is used in the formal verification process. This reduction, when done properly, can result in significant reductions in run times while retaining the possibility of full proofs. This was a very practical talk about the best ways to successfully use formal verification tools.

The second talk, given by Syed Suhaib, was about formal methodologies. Suhaib is the CPU and Tegra formal verification team manager at nVidia. He talked about some of the adoption decisions they have made and the ways in which formal is deployed at nVidia. His talk emphasized the cooperative way in which the design team, the simulation team and his team worked together and how they would often “compare notes” as part of their process.

The final talk was by , who was until last month, a Cadence fellow and developer of COSPAN, a formal verification tool that traces its roots back to 1992. This became the foundational technology for the Cadence FormalCheck tool. Kurshan talked about the way it is easy to lose sight of the real verification goals and provided the example of cache coherence as only being part of the memory system. He said that by verifying the algorithm, it is possible to miss a failure of the system to perform as expected when the entire memory sub-system is considered.

It is good to see this kind of event happening and in a non-commercial setting. While Oski and their sponsors certainly want to get their names attached to formal verification, the event probably mentioned just about every formal tool on the market today and almost no commercial tool was central to any talk or the discussion that I was privy to at the event. Oh – and I nearly forgot to mention – there is a free lunch thrown in as well, plus tickets for the Museum. Unfortunately, that will have to wait for another time because I had a flight to catch.