Empowering Computer Chip Design through Formal Methods

University College London
Computer Science

With a combined $100 billion investment into resilient computer chip supply chains, via the recent US CHIPS Act and European Chips Act, the national importance of semiconductors is recognised at the highest levels of government. From within one of the world's largest chip design companies, I have witnessed the dramatic shift in focus of the sector, driven by the AI revolution. Both academic and industrial attention has moved from traditional processors to massively parallel chips capable of processing vast amounts of data. With all this investment and change, it may come as a surprise that nearly all engineers designing digital circuits, the core building blocks of a computer chip, are using the same proprietary circuit design tools. My experience building graphics processing units (GPUs) at Intel has given me direct insight into how entrenched design technologies—which have remained largely unchanged for decades—operate as slow black boxes that impede innovation.

The ambitious goal of my fellowship is to enable engineers to efficiently explore innovative designs for computational components and produce high-performance parallel chips that are mathematically proven to be functionally correct. To enable efficient exploration, I propose a unique high-level language that bridges the gap between mathematical specifications and low-level circuit optimisations. Radically new open design tools will leverage recent advances in multi-level optimisation to transform easy to write high-level designs into manufacturable circuits that outperform those produced by proprietary tools. Scalable proofs will be generated by a novel orchestration of interacting verifiers, alleviating the fear of uncorrectable hardware bugs. Like a safety rope that empowers climbers to reach new heights without fear of falling, formal methods give designers the confidence to pursue more ambitious solutions. To engage the chip-design community the proposal includes open design competitions and industrially relevant benchmarks that yield countless new research questions.

Revolutionary design tools will allow engineers to innovate with confidence and unlock significant advances in chip performance, enabling new applications, and chip efficiency, reducing the AI climate impact. The fellowship will allow academics, start-ups and technology companies to develop high-performance chip designs in record time and at a fraction of the cost.