So What’s Formal Verification Anyway?

John Harrison has a publicly available presentation from which I have extracted:

Traditionally, errors in hardware and software have been discovered empirically, by testing them in many possible situations.
However, the number of possible situations is usually so large that we can only exercise a tiny proportion of them.
[…]
Formal verification is an alternative that involves trying to prove mathematically that a computer system will function as intended.

For instance, let’s say you’ve developed a smart, optimized piece of hardware for multiplying two numbers. You would want it to behave just like the highly transparent schoolbook version, only you’ve made it much more efficient. One way of convincing the world your new hardware does what you claim is to show lots of examples where it produces the same result as any other comparable device. This would be convincing but not something anyone would bet, say, a multi-billion dollar Mars expedition on. To achieve a higher level of confidence you would need to test that for every input of two numbers the new hardware produces the same result as any other comparable device. Here we are starting to get a sense of the problems ahead. John Harrison again:

For example, there are about 2**80 double extended precision floating point numbers. Testing an operation on all of them will probably never be feasible, even if it’s only unary.
Pre-silicon testing of microprocessor designs is especially limited, since everything is run on simulators orders of magnitude slower than real hardware.

In the latest couple of decades we have seen some remarkable progress when it comes to what is actually feasible using formal verification. This is due to advancements both in technology (the tools have developed) and in application (engineering).

There are today many publicly available tools (just search the subject and you will find) that are accessible to anybody with some interest in the subject. One such tool is used in the puzzle generator for Chrome-8.

One Response to “So What’s Formal Verification Anyway?”

  1. […] short page on Formal Verification. /M var addthis_language = […]