If you were wondering whether formal verification is becoming a cornerstone of mainstream verification flows, several events at the recent DVCon USA 2016 should leave you without any doubt. Consider the evidence:
* The consensus of the panel on “Emulation + Static Verification Will Replace Simulation”
First, out of all the possible topics for a panel on “futures”, this one was chosen (vs. a panel on something really futuristic, like “Is Quantum Computing Ready for EDA?”), suggesting that formal is collectively at the top of people’s minds when they step back and assess the effectiveness of their verification flows today.
Of course, the panel’s animating question was chosen to be deliberately provocative – harkening back to the first wave of formal, with its claims of formal being able to eliminate the need for simulation. However, the panelists – who were heavily weighted toward formal expertise – didn’t renew or update this boast. Instead, they spoke of how formal can be incredibly effective in solving quite a few types of verification challenges, and flatly awful at others. Same goes for simulation and emulation. The consensus that emerged can be paraphrased as, “use the right tool for the job” and “because there are so many different jobs to be done, every verification environment should use formal, simulation, and emulation to some degree”. The larger point here is that in the eyes of these verification experts, formal apps and classical property checking have clearly matured into being an essential component of a complete verification tool kit.
* The formal-specific elements of the EDA CEO keynote
Mentor’s CEO Wally Rhines gave a very expansive keynote – part history lesson, part “state of the art today” snapshot, and part future outlook (Article; Wally’s slides). In synchronicity with the aforementioned panel discussion (that followed right after his speech, so he couldn’t likely have known the independent panel’s consensus beforehand), woven into his remarks were multiple examples of how formal is (A) the exact right tool for the job for several critical verification tasks (e.g. CDC, SoC Connectivity verification, code coverage unreachability & closure, X-corruption, secure path verification, etc.), and (B) is an integral part of a complete verification flow comprised of virtual prototyping, formal, simulation, emulation, and FPGA prototyping.
* The Thursday afternoon tutorial on pure formal basic training was a full house
I don’t mean to brag [ok, I do, just a little], but the tutorial I produced on “Back to Basics: Doing Formal the Right Way” on the last day in the last time slot of the conference – i.e. a historically challenging time slot to draw a sizable audience – was a full house! Apparently, our intuition was correct: there IS a new generation of D&V engineers who are very interested learning classical formal property checking (whether they were inspired by the success with an automated formal app, or sensed the technology is truly ready for prime time). Granted, there were quite a few familiar faces from prior events who no doubt knew of my colleagues Doug Smith and Mark Eslinger’s abilities to distill complex topics into concise, actionable examples. But speaking as a veteran DVCon tutorial producer and presenter, I would have been happy with a gentleman’s 40-45 attendees. Thus we were positively stunned when we filled the room with 70+ people, and held them throughout the length of the program.
Do you agree — are we in a new wave of formal? Please share your thoughts in the comments below, or contact me offline.
Joe Hupcey III