{"id":14467,"date":"2020-08-04T16:33:16","date_gmt":"2020-08-04T23:33:16","guid":{"rendered":"https:\/\/blogs.mentor.com\/verificationhorizons\/?p=14467"},"modified":"2026-03-27T08:45:50","modified_gmt":"2026-03-27T12:45:50","slug":"dac-2020-paper-report-easy-deadlock-verification-and-debug-with-advanced-formal-verification","status":"publish","type":"post","link":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2020\/08\/04\/dac-2020-paper-report-easy-deadlock-verification-and-debug-with-advanced-formal-verification\/","title":{"rendered":"DAC 2020 Paper Report: Easy Deadlock Verification and Debug with Advanced Formal Verification"},"content":{"rendered":"

\"\"<\/a>At this year\u2019s Design Automation Conference (DAC), Formal verification was everywhere \u2013 in posters, papers, and panel discussions \u2013 where new and long-time formal users alike shared their experiences in applying this powerful technology to challenging real-world verification problems. Indicative of this trend was the Best Paper winner, 4.1 Easy Deadlock Verification and Debug with Advanced Formal<\/em>, by lead authors Laurent Arditi and Vincent Abikhattar of Arm<\/a>.<\/p>\n

At a very high-level, Laurent and Vincent were addressing the same deadlock verification issues and employing the same formal-based methodologies outlined in a prior Verification Horizons article, Deadlock Prevention Made Easy with Formal Verification<\/em><\/a>. To briefly re-cap, there are two deadlock scenarios to look out for:<\/p>\n

A<\/strong> – The design gets into a state that it can never escape and there is no sequence of inputs you can give it to dislodge it from that state. This is always a bug that needs to be fixed.<\/p>\n

B<\/strong> – The design gets into a state that it can actually escape, but the system might tend to hang-up there anyway. Depending on the system\u2019s requirements, this is not always a design issue that needs to be fixed; but it\u2019s essential to understand the behavioral boundaries of the logic to confirm there won\u2019t be any trouble.<\/p>\n

Of course, Arm\u2019s DUTs are seriously large IPs that could find their way into a trillion devices<\/a>. Specifically, they shared three case studies where formal-based deadlock analysis with Questa PropCheck<\/a> either found show-stopper bugs, or mathematically proved the absence of deadlock for all time and all inputs.<\/p>\n

1 – Instruction Fetch unit FSMs<\/strong> \u2013 while these FSMs were designed to be resilient in the face of incorrect or unexpected environment behaviors, and sometimes even support Case B above where the DUT can hang out in a given state, their formal analysis showed inescapable deadlocks. (And apparently the performance exceeded expectations, as \u201cProof time is a few minutes, with no overhead for also running the unescapable deadlock checks<\/em>\u201d)<\/p>\n

2 – L1 data cache arbiter<\/strong> \u2013 in this case \u201call assertions were proven<\/em>\u201d \u2013 no doubt a big relief to the project team!<\/p>\n

3 – Credit based protocol verification<\/strong> \u2013 they were able to prove that \u201cno credit is lost<\/em>\u201d, and there were \u201ca few critical bugs found<\/em>\u201d<\/p>\n

My notes aren\u2019t doing this presentation justice, so I urge you to watch the recording when it becomes available. In the meantime, in the DAC proceedings look for the file \u201cB1094_4_1_Arditi_POSTER_1592757546.pdf\u201d<\/p>\n

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

Joe Hupcey III,
\nfor the Questa Formal team<\/p>\n

 <\/p>\n

P.S. Full disclosure: myself and my colleague Jeremy Levitt supported Laurent and Vincent by providing feedback on their slide drafts, and they returned the favor by honoring us as co-authors.<\/p>\n","protected":false},"excerpt":{"rendered":"

At this year\u2019s Design Automation Conference (DAC), Formal verification was everywhere \u2013 in posters, papers, and panel discussions \u2013 where…<\/p>\n","protected":false},"author":71594,"featured_media":15371,"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":[319,342,410,418,492,493,665],"industry":[],"product":[],"coauthors":[],"class_list":["post-14467","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-news","tag-57dac","tag-arm","tag-dac-2020","tag-deadlock-verification","tag-formal-property-checking","tag-formal-verification","tag-questa-propcheck"],"featured_image_url":"https:\/\/blogs.sw.siemens.com\/wp-content\/uploads\/sites\/54\/2020\/08\/easy-deadlock-verification-and-debug-with-advanced-formal-1.jpg","_links":{"self":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/14467","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=14467"}],"version-history":[{"count":1,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/14467\/revisions"}],"predecessor-version":[{"id":15372,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/14467\/revisions\/15372"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media\/15371"}],"wp:attachment":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media?parent=14467"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/categories?post=14467"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/tags?post=14467"},{"taxonomy":"industry","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/industry?post=14467"},{"taxonomy":"product","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/product?post=14467"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/coauthors?post=14467"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}