{"id":11465,"date":"2015-04-16T07:30:54","date_gmt":"2015-04-16T14:30:54","guid":{"rendered":"https:\/\/blogs.mentor.com\/verificationhorizons\/?p=11465"},"modified":"2026-03-27T08:35:58","modified_gmt":"2026-03-27T12:35:58","slug":"do-formal-apps-help-dv-engineers-cross-the-chasm-into-direct-formal-property-checking-this-oracle-case-study-suggests-they-do-part-2-of-2","status":"publish","type":"post","link":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2015\/04\/16\/do-formal-apps-help-dv-engineers-cross-the-chasm-into-direct-formal-property-checking-this-oracle-case-study-suggests-they-do-part-2-of-2\/","title":{"rendered":"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)"},"content":{"rendered":"

Do automated formal apps<\/a> really help D&V engineers \u201ccross the chasm\u201d and start using formal verification directly? In Part 1 of this case study on Oracle\u2019s \u201cProject RAPID\u201d<\/a>, the Oracle team\u2019s appetite for using formal verification was whetted by impressive results from the Questa Connectivity Check<\/a> and Questa Register\u00a0Check<\/a> 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<\/a> for classical model\/property checking. Ram writes:<\/p>\n

\u201cSome of the IP units \u2026 were good candidates for formal verification<\/strong>. That\u2019s 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<\/strong>.\u201d<\/em><\/p><\/blockquote>\n

and<\/p>\n

\u201cSpurred 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.<\/strong> Unlike Assurance, Bug Hunting doesn\u2019t 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.\u201d<\/em><\/p><\/blockquote>\n

\"2015-4-8
\nThe 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!
\n<\/strong><\/p>\n

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 \u2013 i.e. \u201cusing the best tool for the job\u201d 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\u2019s conclusion begins with this observation:<\/p>\n

\u201cFormal 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.<\/strong>\u201d<\/em><\/p><\/blockquote>\n

 <\/p>\n

The bottom-line: formal has \u201cgone mainstream\u201d in this team\u2019s current and future projects:<\/strong><\/p>\n

\u201cThe 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, \u2018I 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.\u2019<\/strong> \u2026 \u201cthe 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.\u201d<\/em><\/p><\/blockquote>\n

 <\/p>\n

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 \u2013 let alone their project\u2019s impressive results \u2013 appear to conclusively prove the original thesis.\u00a0 Namely, once formal\u2019s 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\u2019s verification tool kit<\/strong>.<\/p>\n

Does Ram\u2019s\/Oracle\u2019s journey resonate with you? Have you had the same experience or seen something similar at your employer or clients?\u00a0 Please share your thoughts in the comments below, or contact me offline.<\/p>\n

Until next time, may your coverage be high and your power consumption be low,<\/p>\n

Joe Hupcey III<\/p>\n

 <\/p>\n

 <\/p>\n

 <\/p>\n

P.S. FYI, the author of the Verification Horizons<\/em><\/strong> 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 \u201cI Created the Verification Gap<\/em>\u201d by Ram Narayan and Tom Symons of Oracle Labs<\/a>.\u00a0 Congratulations Ram and Tom!<\/p>\n

 <\/p>\n

Reference Links:<\/strong><\/p>\n

Verification Horizons, March 2015, Volume 11, Issue 1:<\/a>
\n Evolving the Use of Formal Model Checking in SoC Design Verification<\/em><\/a>
\nRam Narayan, Oracle Corp.<\/p>\n

https:\/\/verificationacademy.com\/verification-horizons\/march-2015-volume-11-issue-1\/Evolving-the-Use-of-Formal-Model-Checking-in-SoC-Design-Verification<\/a><\/p>\n

—–<\/p>\n

DVCon USA, March 2014, 1P.2:<\/a>
\n \u201cThe Future of Formal Model Checking is NOW! Leveraging Formal Methods for RAPID System On Chip Verification<\/em>\u201d<\/a>, (Poster Presentation Honorable Mention)
\nRam Narayan, Oracle Corp.<\/p>\n

 <\/p>\n

http:\/\/events.dvcon.org\/events\/proceedings.aspx?id=163-1-P<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"

Do automated formal apps really help D&V engineers \u201ccross the chasm\u201d and start using formal verification directly? In Part 1…<\/p>\n","protected":false},"author":71594,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"spanish_translation":"","french_translation":"","german_translation":"","italian_translation":"","polish_translation":"","japanese_translation":"","chinese_translation":"","footnotes":""},"categories":[1],"tags":[368,443,489,491,492,493,506,557,618,649,661,665,666,680,722,723],"industry":[],"product":[],"coauthors":[],"class_list":["post-11465","post","type-post","status-publish","format-standard","hentry","category-news","tag-bug-hunting","tag-dvcon-best-paper","tag-formal-assurance-strategy","tag-formal-model-checking","tag-formal-property-checking","tag-formal-verification","tag-functional-verification","tag-ip-core-logic-verification","tag-oracle","tag-property-checking","tag-questa-connectivity-check","tag-questa-propcheck","tag-questa-register-check","tag-register-assurance-verification","tag-soc-connectivity-checking","tag-soc-dv"],"_links":{"self":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/11465","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/users\/71594"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/comments?post=11465"}],"version-history":[{"count":1,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/11465\/revisions"}],"predecessor-version":[{"id":19783,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/11465\/revisions\/19783"}],"wp:attachment":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media?parent=11465"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/categories?post=11465"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/tags?post=11465"},{"taxonomy":"industry","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/industry?post=11465"},{"taxonomy":"product","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/product?post=11465"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/coauthors?post=11465"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}