Corner case bugs – Formal got you covered
Imagine the scene. It’s Friday night, and you’ve decided to relax and watch a movie. Given the overwhelming amount of choices, you’ve already spent over an hour watching trailers to choose the movie and you’re finally almost ready to go. All that’s left is the popcorn. You go over to the microwave and get it going. For a little while nothing happens, but then you start to hear the pops, slowly at first but then much more rapidly before beginning to taper off. You then have to ask yourself: When do I stop? This is a big question. Take it out too soon and you’re going to break your teeth on those unpopped kernels. Leave it in too long and you risk burning it. How can you know if its popped long enough?
The popcorn problem is an analogy I often like to use for verification as it’s a problem that all engineers working in the field have to deal with. We all have deadlines but we all want to make sure that there are no bugs sitting in the design. Who knows what’s hiding in those unpopped kernels? How can we really know that we aren’t missing some corner case problem? Just because something is a corner case doesn’t necessarily mean it isn’t a big deal. In my experience I have found corner cases which would cause system lockups, security breaches, non-deterministic behavior and corrupt data to name just a few …and before you close this blog in disgust and have a rant about this narcissistic millennial blog writer, it’s the technology that I’m actually praising here.
Imagine if you could ask your microwave to mathematically prove that your popcorn was going to come out perfectly. If you could ask it to check the kernels and guarantee that they were sufficiently popped. This is what we are trying to achieve by using Formal verification. By design, Formal is going to automatically check all possibilities of input stimulus that could happen and guarantee that properties of your design are true. Of course, this comes with its own set of challenges: building accurate constraints, dealing with bounded proofs etc., but it allows you to ensure that under given constraints something is absolutely correct. By writing really simple properties Formal is able to construct a failure trace that would have otherwise been very difficult to conceive of. Some of the corner case bugs I mentioned earlier were found by writing very simple properties and letting the tool do the hard work.
When you speak to managers who have recently used Formal for the first time, the reaction is often one of being pleasantly surprised. You hear many stories of these strange corner case bugs that Formal found in designs that had already been tested. Huge numbers of issues that have been caught early in the verification cycle and, in a number of cases, ones where designers have had to go back and rewrite their specs.
Using Formal allows you to get that peace of mind that you really have checked all the possibilities and that your popcorn is done to perfection. Now go ahead, put a movie on and chill out, your verification problems are sorted!
