When running Formal Property Verification, we often see goals that are neither proven nor failing (especially on complex properties), which implies inconclusive goals, also referred to as bounded proofs. In these scenarios, what we have at hand is the Formal bounded depth (in terms of clock cycles), associated with such inconclusive properties.
We have been fascinated with the stories of superheroes from X-Men. Who is not impressed with the power of mutation capability of the superheroes? The stories really hit it big when Hollywood became interested in the mid-1990s. Coincidentally, just around the same time formal model checking started to get attention in hardware verification. In those early days, it seemed only people with “superpower” (i.e. PhD in formal verification) knew how to navigate the technology to fully verify and signoff functionality of a design block. It has been a long time since the early days and many new capabilities have emerged to make formal verification easier to do. So, how do people without “superpower” verify and signoff functional verification of design blocks using formal? And do so with absolute confidence?
Sean talked about it in his blog Progression in formal verification – last decade.., Formal verification has come a long way but in most of the first meeting with potential new customers, these are still the most commonly asked questions:
Posted in Formal Methodology