InFormal Chat

Archive for the 'Property Verification' Category

Formal verification on user written properties

 

“Phalanx” – Greek warfare strategy for Formal Property Verification

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.

Continue Reading...

Posted in Formal Methodology, Property Verification

 

Mutation superpower in formal model checking? You betcha!

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?

Continue Reading...

Posted in Formal Methodology, Property Verification

 

Goldilocks and the three constraints!

 

Continue Reading...

Posted in Formal Methodology, Property Verification

 

Progression in formal verification – last decade…..

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.

Continue Reading...

Posted in Property Verification