InFormal Chat

 

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?

A while ago, I was working with a customer to verify a design block using formal model checking technology. We chose Synopsys Formal Property Verification (FPV App) to do this.  We did everything we were supposed to do: we took the design spec, wrote checkers and constraints; we also wrote cover properties to make sure that the list of all the features in the specifications were covered.  We identified some errors in the design, even some missing features.  Designer fixed them and we validated the fixes.  Formal verification has taken on wings in recent years, and more and more features are becoming available including property density, over-constraint, bounded proof as well as formal core coverage.  We utilized these features and analyzed coverage data as well.  When we concluded that we had reached all the functional coverage targets as well as code coverage requirements, we were quite confident that we had done our job and proceeded with the signoff of the functional verification of the design block.

mutation_bug

 

 

The block was integrated in the chip level testing. After some time, it came back with a bug found in the design block that we had signed off.  Oh, no!  What happened?  How could it be possible that this bug escaped our formal testbench?  We could just hear the bug mocking at us.

What more could we have done to safeguard against nasty bugs like this one? Just around that time, another X-Men movie came out.  We were wondering:  Wouldn’t it be great if we can get some super powerful light from Superhero Dazzler to expose this bug so that we can build a better testbench that would have prevented this bug from escaping?  Can we look to X-Men for some answers?

It turned out there was a connection! We were so excited.  Just as genetic mutation enabled ordinary human beings to possess super power, RTL mutation can also provide super powerful metric called fault coverage.

Now, how does RTL mutation work? It does so by inducing mutations (or faults) in RTL code and determine if the verification suite can detect them by executing test-cases.  Here are some examples with the original RTL code on the left, and mutation on the right:

certitude

VC Formal offers an App called Formal Testbench Analyzer (FTA). Combining VC Formal with VCS Fault Injection via RTL mutation, FTA takes fault injected RTL and checks if these faults can be caught by your FPV testbench.  If any of the proven properties in FPV fails because of a fault by mutated RTL code, this fault is declared as “detected”.  If there are faults left as “non-detected”, potential bugs may escape.

We couldn’t wait to give it a try. We took our FPV environment and ran with FTA App.  What we learned was truly astonishing!  Not only FTA helped us uncover the bug escaped from us before, it also revealed other faults not detected by any checkers, therefore exposing more potential weakness in our environment.

mutation2

Look who has the power now, you stupid bug!

 

Share and Enjoy:
  • del.icio.us
  • Digg
  • Facebook
  • Google Bookmarks
  • LinkedIn
  • Twitter