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.