Preview of DVCon 2022 — How to Avoid the Pitfalls of Mixing Formal and Simulation Coverage
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.
See you next week!
Joe Hupcey III
Reference Links
The whole DVCon USA 2022 program: https://2022.dvcon.org/program-grid/
