## Sunday, August 30, 2015

### 211: Saving A Few Million Years

Those of you who follow the Math Mutation facebook feed may have noticed that a book I co-authored was just released: "Formal Verification: An Essential Toolkit for Modern VLSI Design". Now, I need to caution you that this is not a Math Mutation book-- it's a technical book, aimed at electrical and computer engineers invovled in chip design. However, I do think Math Mutation listeners might have some interest in the core concepts on which the book is based. So, today I'll try to give you a brief summary of what Formal Verification is, and why it's worth writing a book about.

You're probably aware that modern computer chips are pretty complicated, by many measures the most complex devices ever created by man. For new ones coming out this year, the number of transistors is measured in the billions. So it makes sense to ask the question: how do we know these things will work? It would be prohibitively expensive to just build them first and then test them, so we need to discover and fix as many of the bugs as possible during the design stage. The process of finding these bugs is known as design validation. For many years, the most popular technology used in design validation has been simulation: testing how a software model of the design will behave for various sets of inputs.

Unfortunately, even a simple chip design has so many possible behaviors that there is no way to simulate them all. For example, suppose you are designing a simple integer adder: it will take 2 numbers as inputs, each expressed with 32 bits, or binary digits, which can each be 1 or 0. It will then output their sum. How many possible input sets are there for this design? Since each input has 32 bits, it has 2^32 possible values, thus resulting in 2^64 possible values for the pair. If we assume we have a fast simulator that can check 2^20 values per second, that means that we will need 2^44 seconds to check all possible values-- over half a million years. Most managers are not very happy when given a time estimate on this order to finish a project. And needless to say, most chips sold today are many orders of magnitude more complex than a simple adder.

So, what can we do to make sure our chip designs really will work? A variety of technologies have been developed over the past few decades to try to find a good set of example values to simulate. And they do seem to be doing a decent job: most electronic devices you buy today seem to more-or-less do what you want them to. But it still seems like there should be a better way to validate them: no matter how good you make it, simulation and related methods can never cover more than a tiny portion of your design's possible behaviors.

That's where formal verification comes in. The idea of formal verification is to take a totally different approach: instead of trying specific values for your design, why not just mathematically prove that it will always be correct? That way you don't have to worry about trying every possible test case. If there is a single set of values that would generate an incorrect result, your proof will fail, and you will know your design has a bug. If you do succeed in mathematically proving your design correct, then you know that there is no bug, and do not need to waste time simulating lots of testcases. In effect, formally verifying a design is equivalent to simulating all possible values. Many would argue that philosophically, this is really the "right" way to validate chip designs. You may have heard the famous Guindon quote, "Writing is nature’s way of letting you know how sloppy your thinking is." Formal Verification pioneer Leslie Lamport expanded on this with "Math is nature's way of letting you know how sloppy your writing is.", and later added "Formal math is nature's way of letting you know how sloppy your math is."

You've probably guessed by now that there has to be a catch. Formal verification is easier defined than done: when billions of transistors are involved, how do we even get our heads around the problem of creating mathematical proofs? It's far beyond what anyone could manually do, so to make this method a possibility, humans need to be aided by intelligent software that helps to automate proofs. To further complicate matters, it's also been shown that any formal verification system needs to internally solve what are known as NP-complete problems. If you remember our discussion way back in episode 13, an NP-complete problem is "provably hard" in some sense, meaning that no piece of computer software can ever solve it efficiently in 100% of cases. However, researchers have worked for many years to try to develop practical software that could utilize clever tricks to enable real proofs on a wide variety of actual industrial product designs.