3 Notable Formal-Related Conference Papers of 2014
2014 was an exciting year for formal verification to say the least, and below I call out a sampling of noteworthy conference papers that contributed to this energy. Specifically, they show how formal property checking itself is simultaneously scaling to tackle ever larger verification problems, and also being extended to cover domains that were once exclusively the province of simulation.
———-
Conference: DVCon 2014
Title: Sign-off With Bounded Formal Verification Proofs
Highlights: This paper totally busts the myth that you need to fully solve a formal proof in order to be valuable for verification. Instead, the authors’ show how “bounded proofs” – i.e. formal proofs that haven’t reached a solution yet – can provide engineers enough information to confidently make sign-off decisions. Specifically, they show that as long as a given formal analysis isn’t failing as it proceeds deeper in to the state space, and as long as it touches the cover points you wanted to hit, “no news is good news” and the design is likely sound.
Authors: NamDo Kim and Junhyuk Park of Samsung Electronics Co., Ltd.; HarGovind Singh and Vigyan Singhal of Oski Technology, Inc.
Proceedings: http://events.dvcon.org/events/proceedings.aspx?id=163-2
———-
Conference: Mentor Graphics’ User2User Conference, San Jose, CA, April 2014
Title: Targeted Approach to Formal Model Checking: A Case Study
Highlights: This paper documents a real work SoC verification case study on how formal was focused on three major verification flows: bug hunting, “assurance” (a/k/a proofs of key functions), and exhaustive static & temporal connectivity checking. The results were impressive: in 50% of the time vs. the simulation approaches they supplanted, these formal applications found 4 RTL bugs missed by other methods, and 6 more RTL bugs in cache verification – 1 of which would have been a chip killer had it escaped.
Author: Ram Narayan, Oracle Labs
Proceedings: http://supportnet.mentor.com/member/u2u/2014-san-jose.cfm
———-
Conference: Mentor Graphics’ User2User Conference, Bangalore India, October 2014
Title: Gear up ! Speed up ! – Dead Code Detection Through Reachability Analysis (D2CTRA) for Coverage Convergence
Highlights: For D&V engineers, few things in verification are more frustrating than watching the code coverage score plateau well short of your coverage spec. No matter how many clever directed test you write, no matter how many different random seeds you try, the coverage score simply flat-lines. In parallel, specifying waivers to deliberately exclude unused IP configurations from the analysis can be a tedious and error prone manual process. In this presentation the authors show how they used Questa CoverCheck to solve this problem on a very control intensive design. In a nutshell, they were able to rapidly identify dead code areas, easily set coverage waivers on properly dead areas to keep them from inaccurately pulling down the coverage score, and investigate and fix the trouble spots. (Note: this presentation won the “Best Paper” award for the conference’s functional verification track!)
Authors: Pandithurai Sangaiyah, Anand Kumar of Qualcomm India Pvt Ltd
Proceedings: https://verificationacademy.com/resource/42639
———-
Again, the above is just a sampling of the great work and innovations being made in the formal and assertion-based verification domain in 2014. 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, 2015 promises to be an even bigger year for formal-based solutions!
Joe Hupcey III
P.S. Bonus: I’ve already written about the ARM Techcon 2014 paper on Advanced Verification Management and Coverage Closure Techniques by Nguyen Le, Microsoft, et.al.; but it bears re-referencing my prior Verification Horizon’s post on this paper: ARM® Techcon Paper Report: How Microsoft Saved 4 Man-Months Meeting Their Coverage Closure Goals Using Automated Verification Management & Formal Apps
Comments