Do Formal Apps Help D&V Engineers Cross the Chasm Into Direct Formal Property Checking? This Oracle Case Study Suggests They Do (Part 1 of 2)
One of the biggest developments in the formal verification world in the past several years has been the industry-wide growth of formal-based “apps” — automated applications that leverage formal’s exhaustive verification technology “under the hood” to focus on specific verification tasks well suited to formal algorithms. But do formal apps really help D&V engineers “cross the chasm” and start using formal verification directly? (Or if you prefer, are apps an effective “Trojan Horse”?) A recent article in Verification Horizons by Oracle’s Ram Narayan titled “Evolving the Use of Formal Model Checking in SoC Design Verification” about the evolution of the verification methodology employed on Oracle’s “Project RAPID” suggests the answer is “yes”.
In a nutshell, the clear benefits Ram’s team received from formal apps inspired them to try their hand at formal model checking; and their results exceeded all expectations. I recommend you read the article in its entirety because it’s a great real-world case study; rich with anecdotes from the front-line engineer himself. (Indeed, this article was inspired by Ram’s award winning DVCon 2014 poster, but I digress) But for the purposes of this post, allow me to focus exclusively on the highlights pertaining to the “crossing the chasm” thesis. Consider the following excerpts.
* First, they started from scratch:
“At the outset of the project, there were no specific plans to use formal verification on RAPID. We did not have any infrastructure in place for running formal tools, and neither did we have anyone on the team with any noteworthy experience using these tools.”
* The first app they tried exceeded all expectations: Like many customers, Oracle got their feet wet with formal-driven SoC connectivity checking. And like 100% of Questa Connectivity Check app customers, they came away impressed:
“Our goal was to catch trivial design errors through formal methods without having to rely on lengthy and in some cases, random SoC simulations. Given our modest expectations at the outset, we would have been satisfied if we just verified these SoC connectivity checks with formal tools. … SoC Connectivity checks were written to verify the correct connectivity between critical SoC signals like interrupts, events and other control/datapath signals. These checks are trivial to define and are of high value. Proving these connections saved us significant cycles in SoC simulations.”
This is not just a gut feeling on the author’s part: the bottom row of Table 2 in the article (showing the Questa Connectivity Check app cutting the schedule by 66%) backs-up the above quote with real project data.
* Another app is tried, and it’s also wildly successful: the Questa Register Check app was the next formal app to be applied. Not only did it take care of the immediate control&status register verification task, but it also enabled more effective downstream verification:
“The Register Access Verification established controllability and observability of the registers in the unit from its interface. The IP core logic verification could now safely use the control registers as inputs to properties on the rest of the logic they drive. In addition to these registers, we chose a few internal nodes in the design as observation and control points in our properties. These points gave us additional controllability and observability to the design and reduced the complexity of the cones of logic being analyzed around them. We proved the correctness (observability) of these points prior to enjoying the benefits of using them (controllability) for other properties. This approach made it easier to write properties on the entire unit without any compromise on the efficacy of the overall unit verification.”
At this point in the story, the Oracle team is still confining their use of formal to the stable of available automated formal apps. However, as we’ll see in Part 2 of this case study, this success bred curiosity in the underlying technology …
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.
