FMCAD 2019: The Most Important Formal Verification Conference You’ve Never Heard Of
[Preface: I briefly interrupt my series on The Many Flavors of Equivalence Checking to share this report on an important formal technology conference.]
As far as formal verification has come in the past 30 years, in many ways it is just the “end of the beginning” as per the steady growth of its commercial application in ASIC, FPGA, and System design and verification. The source of this progress can be traced to the ongoing research in formal algorithms, which is shared on an annual basis at the Formal Methods in Computer Aided Design (FMCAD) conference.
The Questa Formal R&D team (a/k/a ex- 0-In R&D) attends every year to keep abreast of the latest developments in the field, and they always come away inspired with new ideas that ultimately improve the performance of our products. In this post, Questa Formal R&D lead Dr. Jeremy Levitt shares his take-aways from this year’s event.
Joe: First, tell me more about the conference.
Jeremy: This sentence on the event’s home page sums it up nicely, “FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems.”
But this belies the surprisingly broad scope of the conference: you might think formal methods are only for digital circuity or discrete systems, so it might surprise you to learn that there were sessions on theorem proving for verification of analog and mixed-signal circuits, as well as on applying formal verification to blockchain systems. This wide range of topics – and the variety of perspectives of the presenters – makes this conference thought-provoking for all the attendees. Granted, it can often be a stretch to imagine how the ideas and algorithms in some of these papers can map to mainstream EDA and functional verification. But that’s part of the fun – and a key driver for innovating our way out of the most difficult challenges we face.
Joe: With that said, what has been rolling around in your mind since the conference?
Jeremy: A lot! <<< Laugh >>> Again, the conference provided much food for thought, but I will concede that there is one session that stands out for me: “Challenges and Solutions in Post-Silicon Validation of High-end Processors”. Obviously in a perfect world the PRE-silicon verification would be 100% effective, but sadly bugs do slip through even the most well-constructed and maintained verification nets. When this happens, it can be incredibly hard to find the root cause of an intermittent failure. The process of coordinating formal analysis with assertion-based and constrained-random simulations, in parallel with the live hardware testing, can get out-of-hand without the right strategy, execution, and results sharing. Avi Ziv’s tutorial on IBM’s methodology and framework for on-chip testing — having the processor generate and run tests on itself — highlights a crucial part of the verification flow that does not get enough attention from the formal verification community. IBM’s is truly a best practice approach, and begs the question: how can we apply formal verification at the post-silicon verification phase as effectively as we apply it in the pre-silicon verification phase?
Joe: Referring to all the papers on new formal algorithms and analysis techniques, what are the implications for the formal engines under-the-hood of our Questa Formal apps?
Jeremy: I don’t want to give too much away because the ideas and discussions that arise from this conference really do inspire cutting-edge enhancements that go into our formal engines. But, looking out in the future, further application of “Quantified Boolean Logic” (vs. the “Quantified Free Logic” approach that we mainly use today) is intriguing, as are the increasingly clever applications of SMT solvers.
Joe: Thanks, Jeremy! Final thoughts?
Jeremy: It bears repeating, I’ve been going to FMCAD since the very first one back in 1996, and every year I’m positively surprised at how the field continues to advance. The stream of novel ideas in the academic, industry, and student tracks are indicative of a robust area of applied mathematics and engineering that has many directions in which to grow. In turn, this source of inspiration will enable the Questa Formal team to stay ahead of our customers’ toughest technical challenges.
Until next time, may your properties be as simple and sequentially short as possible, and all your results be conclusive.
Joe Hupcey III
Reference link:
P.S. The Questa Formal R&D team is hiring! We have an opening in our Fremont, CA office — join us!
