{"id":16949,"date":"2022-02-21T10:25:30","date_gmt":"2022-02-21T15:25:30","guid":{"rendered":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/?p=16949"},"modified":"2026-03-27T08:48:45","modified_gmt":"2026-03-27T12:48:45","slug":"preview-of-formalcon-2022-previously-dvcon-how-to-avoid-the-pitfalls-of-mixing-formal-and-simulation-coverage","status":"publish","type":"post","link":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2022\/02\/21\/preview-of-formalcon-2022-previously-dvcon-how-to-avoid-the-pitfalls-of-mixing-formal-and-simulation-coverage\/","title":{"rendered":"Preview of DVCon 2022 — How to Avoid the Pitfalls of Mixing Formal and Simulation Coverage"},"content":{"rendered":"\n

With eight papers in two separate sessions focused exclusively on formal verification, one could assert (pun intended) that this year\u2019s DVCon USA (February 28-March 3)<\/a> has in some ways become \u201cFormalCon\u201d. On the agenda is a well curated mix of novice, intermediate, and expert-level papers that go into formal methods in-depth; as well as show how formal can be effectively integrated with other verification approaches. In regard to this second case, allow me to share a sneak-preview of the paper by my colleagues Mark Eslinger and Nicolae Tusinschi that I\u2019ve been proud to support: How to Avoid the Pitfalls of Mixing Formal and Simulation Coverage.<\/a><\/em> Without giving too much away \u2026<\/p>\n\n\n\n

The most effective functional verification environments employ multiple analysis technologies — static analysis, simulation, formal, hardware-assisted verification, etc. — where the strengths of each are combined to reinforce each other to ensure that the Device Under Test (DUT) behaves as specified. However, this creates an inherent challenge of properly comparing and combining the results from each source to give a succinct, accurate picture of the verification effort\u2019s true status. Spoiler alert: simply merging coverage measurements from different sources — in particular, blindly combining coverage from constrained-random simulations and formal analysis — can fool the end-user into believing that they have made more progress, and\/or they have observed behaviors of importance, when neither is the case.<\/p>\n\n\n\n

Among some of the issues that come into play:<\/p>\n\n\n\n

\u2022 Simulation coverage only reflects specific forward paths the simulation has traversed from the inputs through the state space, for a specific set of stimuli.<\/p>\n\n\n\n

\u2022 Some types of formal coverage do reflect a \u201cforward traversal\u201d, but just because the formal analysis might traverse some of the same states as a simulation, the logic \u201ccovered\u201d is usually greater. Additionally, the formal analysis has free-floating input stimulus, and is valid for all time. <\/p>\n\n\n\n

\u2022 Other types of formal coverage report how logic and signaling \u201cworks backwards\u201d from an output.<\/p>\n\n\n\n

So what\u2019s a verification engineer to do???<\/p>\n\n\n\n

To find out, They\/You will just have to tune-in to the \u201cFormal Verification 1\u201d session at DVCon USA 2022 next Tuesday March 1 at 3pm Pacific \u2013 paper 1086<\/a>.<\/p>\n\n\n\n

See you next week!<\/p>\n\n\n\n

Joe Hupcey III<\/p>\n\n\n\n

<\/p>\n\n\n\n

Reference Link<\/strong>s<\/p>\n\n\n\n

The whole DVCon USA 2022 program: https:\/\/2022.dvcon.org\/program-grid\/<\/a><\/p>\n\n\n\n

Overview of Siemens EDA @DVConUS 2022<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"

With eight papers in two separate sessions focused exclusively on formal verification, one could assert (pun intended) that this year\u2019s…<\/p>\n","protected":false},"author":71594,"featured_media":16948,"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":[1002,395,401,402,448,493,718],"industry":[],"product":[],"coauthors":[931],"class_list":["post-16949","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-news","tag-1002","tag-constrained-random-simulation","tag-coverage","tag-coverage-closure","tag-dvcon-u-s","tag-formal-verification","tag-simulation"],"featured_image_url":"https:\/\/blogs.sw.siemens.com\/wp-content\/uploads\/sites\/54\/2022\/02\/DVCon-USA-2022-How-to-Avoid-the-Pitfalls-of-Mixing-Formal-and-Simulation-Coverage-scaled.jpg","_links":{"self":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/16949","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=16949"}],"version-history":[{"count":5,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/16949\/revisions"}],"predecessor-version":[{"id":16977,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/posts\/16949\/revisions\/16977"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media\/16948"}],"wp:attachment":[{"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/media?parent=16949"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/categories?post=16949"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/tags?post=16949"},{"taxonomy":"industry","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/industry?post=16949"},{"taxonomy":"product","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/product?post=16949"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/wp-json\/wp\/v2\/coauthors?post=16949"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}