Chips with confidence

Collaboration between the University of Oxford and Intel Corporation has developed new methods to check that electronic chips do what they’re meant to do, before they are manufactured.

Integrated electronic chips, such as the processor in a laptop, contain many billions of interconnected transistors, all working together to run programs. The engineering design of a new chip is extremely challenging, and ensuring that the finished chip works correctly is vitally important. Almost half of the several years spent creating a new chip goes on testing it for potential errors.

Fabricating a prototype chip to test a design is prohibitively expensive, so computer simulations are widely used to validate designs. But exhaustive simulation of every possible internal set of connections in every possible operating condition would take many millions of years to test a chip exhaustively, so is clearly not feasible.

Tom Melham, Professor of Computer Science at the University of Oxford, has been working with Intel Corporation since the late 1990s to develop and apply a mathematical validation technique known as formal verification. This entails building a mathematical description of the chip design and then analysing its correctness by rigorous mathematical proof. The proofs are very large, so a simplification technique called abstraction is used to pick out salient features for testing; one such technique has been patented by Intel and Professor Melham. Twenty-five years ago these advanced formal verification techniques were thought unachievable; today they are in routine use by Intel and other companies worldwide.

Professor Melham’s collaboration with Intel is a prime example of knowledge exchange between academia and industry. Intel, led by experts such as Senior Principal Engineer Dr Carl Seger, has pioneered the use of formal verification on the hardest industrial chip design problems. Melham has worked closely with Intel engineers for over a decade, and Intel researchers have spent time at the University of Oxford – including Dr Seger as a Visiting Fellow of Balliol College during 2006-7.

The ability to rapidly identify design errors in a chip is cost-effectively driving forward new designs that use less power and are more environmentally friendly. The technique also has applications in safety-critical systems, such as aeroplane, automotive, or rail control, where confidence in the chips is vital.

Funded by: Intel Corporation and the Engineering and Physical Sciences Research Council.