Checking hardware equivalence checkers

点击翻译按钮获取中文摘要

CONTEXT. Hardware synthesis tools often rely on "equivalence checkers" to establish that the output design remains behaviourally equivalent to the input design. 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_, which means that if they make a mistake and claim, for instance, that two designs are equivalent when they are in fact not, then the final hardware could contain a bug. And bugs in hardware can be extremely expensive to rectify.PROJECT OBJECTIVES. We intend to establish whether these equivalence checkers are in fact _trustworthy_. Do they contain bugs that undermine the reliability of the hardware designs they generate? And if so, can we devise testing or verification techniques that could help to make equivalence checkers more trustworthy? METHOD. We will design new testing techniques for equivalence checkers. This will likely be based around the generation of large numbers of random hardware designs, together with the application of random mutations to these designs, in order to obtain a corpus of not-quite-equivalent pairs of hardware designs that can be fed to the equivalence checkers under test. Innovation will be required to devise random generation techniques and random mutation techniques that are biased towards exposing bugs (should they exist) without producing hardware designs that are prohibitively large (and hence slow to synthesise).ALIGNMENT TO EPSRC RESEARCH AREAS. The project aligns with the EPSRC's "Safe and secure ICT" priority by seeking to make hardware synthesis a less bug-prone process. A lot of work is being done on verifying the correctness of designs at higher levels of abstraction; this project complements that work by checking that those correctness guarantees are not ruined when designs are fed into the final "link" in the chain: the synthesis tools. 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 testing techniques such as fuzzing and mutation testing.