Improving the reliability of hardware equivalence checkers

CONTEXT.
Hardware designers often rely on "equivalence checkers" to establish that their hardware designs match high-level specifications. Widely used commercial equivalence checkers include Conformal Equivalence Checker from Cadence, FormalPro-LEC from Siemens, and Formality Equivalence Checking from Synopsys. All of these tools have to be _trusted_. Should they make a mistake, that is, claim that two designs are equivalent when they are in fact not, then the final hardware could contain a bug. Such bugs in hardware can be extremely expensive to rectify.

PROJECT OBJECTIVES.
We intend to establish whether equivalence checkers are in fact _trustworthy_. Do they contain bugs that undermine the reliability of the hardware designs they generate? Furthermore, we intend to devise testing or verification techniques to improve the reliability of equivalence checkers.

METHOD.
We will design new testing techniques for equivalence checkers, based around generating large numbers of random hardware designs pairs, which can be fed to the equivalence checkers under test. In addition to searching for the existence of bugs, we also intend to apply formal verification techniques, using a proof assistant such as Rocq, to prove the _absence_ of bugs from an equivalence checker.

ALIGNMENT TO EPSRC RESEARCH AREAS.
The project aligns with the EPSRC's "Safe and secure ICT" priority by seeking to make hardware design a less bug-prone process. The project also relates to several EPSRC areas of investment and support: "Programming languages and compilers" because a hardware synthesis tool is a specialised type of compiler, "Microelectronics design" because hardware synthesis is a key tool in the hardware design process, and "Software engineering" because the project will build on established software verification techniques such as fuzzing and formal verification.