CREST - C REference model Synthesis Tool: Datapath Formal Verification using CBMC for C Specifications

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.