How to save $500 million: formal proof in the electronics industry

Dr Sam Elliott, Imagination Technologies Limited

In 1994, a bug was found in the floating point division hardware of the Intel Pentium processor. Although estimates vary, Intel claimed a close to $500 million loss on the basis of this single bug, and were left in a precarious position with their reputation, especially in the scientific community, severely hurt. In response, they took a dramatic step, and invested heavily in the little-known technology of computer assisted proof to verify future cores. Now 25 years later, formal mathematical proof is now finally becoming a key technology for verifying digital hardware, and is giving a higher level of confidence than we’ve ever seen, despite the continual increase in design complexity.

We will briefly explore the history of the use of proof in digital electronics, before moving on to some state-of-the-art examples which demonstrate how complex arithmetic hardware is being verified now using mathematical proof techniques. No specific knowledge of digital electronics is required, only basic Boolean algebra and binary arithmetic.

Dr. Sam Elliott is the Principal Datapath Engineer at Imagination Technologies. He joined Imagination 7 years ago after completing his PhD and an associated postdoc at the University of Leeds, under the supervision of Prof. Jonathan Partington. Dr. Elliott now runs a highly regarded applied research team of design and verification engineers focusing on mathematical hardware, primarily for mobile graphics applications. He and his team continue to maintain links with academia, and look to collaborate wherever possible to continue to solve cutting edge problems in industrial mathematics.