Cookies on this website

We use cookies to ensure that we give you the best experience on our website. If you click 'Accept all cookies' we'll assume that you are happy to receive all cookies and you won't see this message again. If you click 'Reject all non-essential cookies' only necessary cookies providing core functionality such as security, network management, and accessibility will be enabled. Click 'Find out more' for information on how to change your cookie settings.

A computer circuit board

PI: Tom Melham

Department: Computer Science

Ensuring the design of a complex computer chip works as intended – before it is manufactured – is technically and financially critical to semiconductor companies. Exhaustive simulation is impossible, so an alternative method called formal verification is sometimes used. This entails creating a mathematical description of the design and checking the design's correctness against this description by computer-aided mathematical proof. Semiconductor manufacturers use very sophisticated software tools to do this, supplied by Electronic Design Automation (EDA) companies.

Checking datapath circuits – the parts of the chip that do arithmetic calculations – is extremely critical. A widespread approach to describing the intended function of datapaths is as a software program, written in C with elements of C++. CBMC, a state-of-the art Oxford research tool, offers the ability to process these programs into a form that can be used by the well-established EDA tools that chip designers use. 

This project will decisively establish the promise of this technology through a focussed, critical-mass prototyping and at-scale demonstration effort. The aim is to bring datapath formal verification into wide industrial usage, exploiting substantial, pre-existing Oxford research IP as a component.

Related themes