Testing and verifying the tools of hardware design

Hardware engineers rely on several tools to build hardware, such as high-level synthesis tools to convert C code into Verilog, logic synthesis tools to convert Verilog into netlists, and so on until they end up with a design that can be implemented on an FPGA or fabricated on an ASIC. Mistakes are difficult and expensive to rectify, so engineers routinely use formal equivalence checkers to double-check that each transformation is correct. All these tools are critical pieces of software infrastructure and are highly trusted... but are they trustworthy? At Imperial, we have been developing new techniques for testing and verifying hardware design tools. We have found bugs in all of the tools we have tested, even the formal equivalence checkers. Some of these bugs cause the tools simply to crash; others are more sinister, causing the tools to produce incorrect results. We are also prototyping new hardware design tools that come with a mechanically checked proof of their own correctness and thus promise the highest standard of reliability. The work is led by my current and former PhD students Yann Herklotz, Quentin Corradi, and Michalis Pardalos, and is also in collaboration with George Constantinides, Alastair Donaldson, Emiliano Morini, and Laura Pozzi.

John Wickerson is a Senior Lecturer in the Department of Electrical and Electronic Engineering at Imperial College London. His research is at the intersection of programming languages and hardware design.