Checking hardware equivalence checkers

上下文硬件综合工具通常依赖于“等价检查器”来确定输出设计在行为上与输入设计保持等价。广泛使用的商业等价检查器包括Cadence的Conformal Equivalence Checking、Siemens的FormalPro-LEC和Synopsys的Formality Equivalence Checking。所有这些工具都必须是可信的，这意味着如果它们犯了一个错误，声称两个设计是等价的，而实际上它们并不等价，那么最终的硬件可能包含一个bug。而硬件中的错误要纠正可能会非常昂贵。我们打算确定这些等价检查器实际上是否是可信的。它们是否包含破坏其生成的硬件设计的可靠性的错误？如果是这样，我们是否可以设计出测试或验证技术，使等价检查器更值得信赖？法我们将设计新的测试技术的等价检查。这将可能基于大量随机硬件设计的生成，以及对这些设计的随机突变的应用，以便获得可以被馈送到测试中的等价性检查器的不完全等价的硬件设计对的语料库。创新将需要设计随机生成技术和随机突变技术，这些技术偏向于暴露错误（如果它们存在），而不会产生过大的硬件设计（因此合成缓慢）。该项目与EPSRC的“安全和可靠的ICT”优先事项保持一致，力求使硬件合成成为一个不太容易出错的过程。在更高的抽象层次上验证设计的正确性方面做了很多工作;这个项目通过检查这些正确性保证不会在设计被输入到链中的最后一个“环节”时被破坏来补充这项工作：合成工具。该项目还涉及EPSRC的几个投资和支持领域：“编程语言和编译器”，因为硬件合成工具是一种专门类型的编译器;“微电子设计”，因为硬件合成是硬件设计过程中的关键工具;以及“软件工程”，因为该项目将建立在模糊和突变测试等既定软件测试技术的基础上。

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.