Chips without bugs: a new software tool for designing computer hardware

Imperial researchers are developing a new way to design more efficient computer chips that are mathematically proven to be free from bugs.

As computers are increasingly entrusted with safety- and security-critical tasks, for example in modern cars where driving decisions are being controlled by a computer, or in national cyber security applications, it’s vital to ensure the computer chips that carry out these tasks are guaranteed to be free of bugs – or faults – before they are even manufactured.

From software program to hardware design

Chip designers use electronic design automation software to model, simulate and optimise designs and test for errors. The job of designing computer chips can be made easier by specifying what the chip needs to do as a software program, a high-level functional description written in computer programming language, and then using an automatic translation tool to turn this program into a detailed manufacturable hardware design.

It’s important that these translation tools do not introduce any bugs, and guarantee that the hardware design, when translated, behaves the same as the software program they are given.

PhD student Yann Herklotz and his supervisor Dr John Wickerson first presented their automatic translation tool – Vericert in 2021. Vericert takes a piece of software written in the C programming language and translates it into a hardware design written in Verilog – a programming language for designing hardware.

Although Vericert’s 2021 hardware designs were guaranteed to be correct – for example if the software was a program that calculates a sequence of prime numbers, the hardware design would be guaranteed to calculate the exact same sequence – their performance was poor; the hardware ran very slowly.

The team has now been able to address this shortcoming, and their new paper describes how they generate hardware designs that are fast and energy-efficient, while preserving the vital mathematically-guaranteed correctness.

They will be presenting their latest advances in Copenhagen next week, at the top international venue for research in programming languages: the ACM conference on Programming Language Design and Implementation (PLDI).

Performing in parallel

John Wickerson explains, “The initial version of Vericert produced simple hardware designs that performed just one step of the computation at a time. This made it easy to prove the translation correct, but it neglected the inherently parallel nature of computer hardware. Computer hardware is made up of loads of “logic gates” all wired together in a big network, with the outputs of one gate being fed into other gates. It’s “inherently parallel” because you can have lots of gates firing at the same time i.e. in the same clock cycle. The new version of Vericert analyses the software, works out which parts of the computation can be done simultaneously, and allocates these parts to hardware clock cycles accordingly.”

“It's a delicate balancing act because if too little computation is done simultaneously then performance deteriorates because too many clock cycles are needed, but too much computation packed into a single clock cycle forces the hardware to run at a slow clock rate, and that spoils performance too!”

The next steps

Vericert already offers a uniquely trustworthy translation tool compared with state-of-the-art ‘unverified’ tools, but Yann and John’s latest developments in performance make it a potentially exciting prospect for the industry, and they are now working on developing more optimisations to further improve its performance.

Yann Herklotz adds “Our next target for Vericert is to add support for loop pipelining, which aims to allow several iterations of a loop to overlap with each other. Once this is implemented, we hope that Vericert will really start to compete with other C-to-Verilog translators, not just in terms of correctness, but in terms of performance too.”