Cookies on this website
We use cookies to ensure that we give you the best experience on our website. If you click 'Continue' we'll assume that you are happy to receive all cookies and you won't see this message again. Click on 'Find out more' to see our Cookie statement.
Crest c reference model synthesis tool datapath formal verification using cbmc for c specifications 2

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.