3 Notable Formal Verification Conference Papers of 2020
On the short list of positive things to come out of the past year are the formal verification-focused conference papers highlighted below. As you will see, there was an interesting mix of how engineers leveraged automated formal applications (such that they didn’t have to learn or directly use formal themselves), and state-of-the-art methodologies for employing property checking directly.
Conference: User2User North America 2020
Title: Achieving 100% Code Coverage: What Used to Be Hard Is Now Easy With an Automated, Exhaustive Flow
Highlights: This presentation shares the experiences of an IP R&D team that specializes in developing highly configurable IPs for very large FPGAs; where their customers demand 100% code coverage and complete documentation of any exclusions (e.g. RTL code that is “legitimately dead” because some legal configuration(s) of a given IP are not being used in a particular end-product).
Manually fixing the “obvious” dead code issues – whether they are from bugs, or easy-to-spot exclusions – gets them to 80-90% code coverage. However, closing the remaining 10-20% of code coverage to meet the 100% requirement was really painful. In parallel, their prior, manual maintenance of exclusions whenever the DUT code changed was very time consuming and error prone. Finally, their products track the releases of new FPGA parts, so each new project is larger – i.e. N^2 more manual inspection time needed (but of course, their head count doesn’t scale to match!)
Their new, automated flow employs the Questa CoverCheck formal app to both exhaustively identify all the dead code, and also automatically maintain the exclusions. Beyond saving them a ton of time, the fact that CoverCheck does an exhaustive formal analysis under-the-hood gives everyone peace of mind that all unreachable code areas have been identified.
Author: Pedram Riahi – Raytheon
Proceedings: https://www.mentor.com/events/user2user-na-virtual
Conference: User2User North America 2020
Title: Exhaustive Verification of SoC Interconnect Including Conditional and Variable Delay
Highlights: Over the past decade, connectivity checking with formal is easily the most popular formal-based application that I’ve seen. It’s easy to see why: the Questa Connectivity Check formal app is significantly faster than any other approach, while simultaneously delivering exhaustive results. Given this app’s maturity, imagine my delight when the authors of this paper shared an innovative, and effective twist to the Connectivity Check flow to address the challenge of verifying interconnect delays that were being added very late in the design cycle (when the pressure is really on to deliver results quickly!).
In a nutshell (and apologies for the oversimplification), in this presentation they show how they were able to build upon a baseline formal analysis to verify all the new signal paths that were being added late in the project; including adding a bit of automation to run the analysis from the bottom-to-the-top of the SoCs hierarchy. With this clever, efficient flow, they found errors with feedthroughs due to mismatched delay in control and data paths, as well as some serious specification bugs that had gone unnoticed.
Authors: Sai Rama Krishna Nalla, Arsen Manukyan, Udupi Harisharan – Cisco Systems
Proceedings: https://www.mentor.com/events/user2user-na-virtual
Conference: 2020 DVCon Europe
Title: Formal Verification Experiences: Silicon Bug Hunt with “Deep Sea Fishing”
Highlights: First, this presentation was the conference’s Best Poster award winner! This came as no surprise to me because the authors did a great job clearly walking the audience through an expert-level application of formal verification: post-silicon bug hunting.
Ideally, in a perfect world bugs would never escape into silicon; but it happens. And when it does, the pressure is on to quickly get to the root cause of the issue and turn-around a fix (which itself does not cause any new, unwanted side-effects). Finding such bugs – and then exhaustively proving that the repair(s) will work and not cause any more trouble – is an in iterative process that requires successful management of numerous factors concurrently. This presentation methodically breaks down the flow into discrete steps, illustrating how it all comes together in the context of two real-word case studies (verification of a DDR3-style memory controller, and an all-new memory controller design).
Bottom-line: if you are already familiar with formal, I think you will come away from this paper with a lot food for thought on how to best approach your next project – whether it’s pre- or post-silicon bug hunting. That said, even if you are just getting started with formal property checking yourself, I dare say that this paper is relatively easy to follow, and thus it will give you some new techniques to quickly leverage.
Authors: Ping Yeung, Mark Handover, Abdel Ayari – Siemens EDA
Proceedings: https://www.dvcon-europe.org/
The above listings are just a sampling of the great work and innovations being made in the formal and assertion-based verification domain today. And if the anecdotes and success stories that I’m regularly receiving in my InBox (let alone the upcoming conference papers and posters that I’m aware of) are any indication, 2021 promises to be an even better year for formal-based solutions!
Joe Hupcey III
P.S. Bonus: I’ve already written about the DAC 2020 Best Paper, Easy Deadlock Verification and Debug with Advanced Formal Verification; but it bears revisiting given how critical it is for many applications to exhaustively prove the design can absolutely never deadlock.
