Do Formal Apps Help D&V Engineers Cross the Chasm Into Direct Formal Property Checking? This Oracle Case Study Suggests They Do (Part 2 of 2)
Do automated formal apps really help D&V engineers “cross the chasm” and start using formal verification directly? In Part 1 of this case study on Oracle’s “Project RAPID”, the Oracle team’s appetite for using formal verification was whetted by impressive results from the Questa Connectivity Check and Questa Register Check apps. Picking up the story where we left off, award-winning author Ram Narayan explains how success with these automated formal apps inspired the team to try their hands at using formal technology directly with the Questa Property Checking (PropCheck) app for classical model/property checking. Ram writes:
“Some of the IP units … were good candidates for formal verification. That’s because it was very reasonable to expect to be able to prove the complete functionality of these units formally. We decided to target these units with the Assurance strategy.”
and
“Spurred by the success of applying [the apps], we considered applying formal methods in a bug hunting mode for units that were already being verified with simulation. Unlike Assurance, Bug Hunting doesn’t attempt to prove the entire functionality, but rather targets specific areas where simulation is not providing enough confidence that all corner case bugs have been discovered.”
The results of their assurance and bug hunting strategies speak for themselves: Table 1 in the article reports that the team found 79 bugs with these formal verification techniques!
Given this success with formal, the team gained the confidence to apply formal in more DUT areas where formal would be more effective than simulation – i.e. “using the best tool for the job” as necessary. Indeed, a common thread throughout the whole story is how formal and simulation were often used in tandem to simultaneously leverage the unique strengths of each technology to improve the overall quality of verification. The article’s conclusion begins with this observation:
“Formal verification is a highly effective and efficient approach to finding bugs. Simulation is the only means available to compute functional coverage towards verification closure. In this project we attempted to strike a balance between the two methodologies and to operate within the strengths of each approach towards meeting the projects goals.”
The bottom-line: formal has “gone mainstream” in this team’s current and future projects:
“The most significant accomplishment to me is the shift in the outlook of the design team towards formal. According to one designer whose unit was targeted with Bug Hunting, ‘I was initially skeptical about what formal could do. From what I have seen, I want to target my next design first with formal and find most of the bugs.’ … “the time savings and improved design quality that formal verification brings are welcome benefits. We plan to continue to push the boundaries of what is covered by formal in future projects.”
Granted, the road from zero formal to full adoption might not have been quite as smooth as this engaging article describes. Still, their declaration to future usage of formal apps in conjunction with formal property checking – let alone their project’s impressive results – appear to conclusively prove the original thesis. Namely, once formal’s considerable power and benefits are introduced by a series of formal apps, there is no going back and formal becomes a permanent part of the user’s verification tool kit.
Does Ram’s/Oracle’s journey resonate with you? Have you had the same experience or seen something similar at your employer or clients? Please share your thoughts in the comments below, or contact me offline.
Until next time, may your coverage be high and your power consumption be low,
Joe Hupcey III
P.S. FYI, the author of the Verification Horizons article described above (and the related award-winning DVCon 2014 poster) was also a co-author of the 2015 DVCon USA Best Paper, 10.1 “I Created the Verification Gap” by Ram Narayan and Tom Symons of Oracle Labs. Congratulations Ram and Tom!
Reference Links:
Verification Horizons, March 2015, Volume 11, Issue 1:
Evolving the Use of Formal Model Checking in SoC Design Verification
Ram Narayan, Oracle Corp.
—–
DVCon USA, March 2014, 1P.2:
“The Future of Formal Model Checking is NOW! Leveraging Formal Methods for RAPID System On Chip Verification”, (Poster Presentation Honorable Mention)
Ram Narayan, Oracle Corp.
