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?
If you have been watching/following the activities in the formal verification domain, you may have noticed an undeniable shift in the market over the last few years.
Posted in Property Verification