Preview of DVCon 2022 — How to Avoid the Pitfalls of Mixing Formal and Simulation Coverage
By Joe Hupcey III • February 21, 2022 • 2 MIN READ
With eight papers in two separate sessions focused exclusively on formal verification, one could assert (pun intended) that this year's DVCon USA (February 28-March 3) has in some ways become "FormalCon". 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've been proud to support: How to Avoid the Pitfalls of Mixing Formal and Simulation Coverage. Without giving too much away …
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's 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.
Among some of the issues that come into play:
• Simulation coverage only reflects specific forward paths the simulation has traversed from the inputs through the state space, for a specific set of stimuli.
• Some types of formal coverage do reflect a "forward traversal", but just because the formal analysis might traverse some of the same states as a simulation, the logic "covered" is usually greater. Additionally, the formal analysis has free-floating input stimulus, and is valid for all time.
• Other types of formal coverage report how logic and signaling "works backwards" from an output.
So what's a verification engineer to do???
To find out, They/You will just have to tune-in to the "Formal Verification 1" session at DVCon USA 2022 next Tuesday March 1 at 3pm Pacific – paper 1086.
Joe Hupcey III
The whole DVCon USA 2022 program: https://2022.dvcon.org/program-grid/
Overview of Siemens EDA @DVConUS 2022
constrained-random simulation
Coverage Closure
DVCon U.S
formal verification
Siemens EDA @DVConUS 2022 February 14, 2022 DVConUS is coming up, beginning on February 28, 2022. The conference will be virtual again for 2022, but I'd like…
The September Verification Horizons is Now Online! September 2, 2021 I'm really excited to share with you a very special issue of the Verification Horizons newsletter for September, 2021. The…
Leave the House With a Clean Design September 14, 2021 Wouldn't it be great if there were something that would stop you from leaving the house wearing mismatched clothes -…
This article first appeared on the Siemens Digital Industries Software blog at 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/