Checking hardware equivalence checkers

上下文。硬件合成工具通常依赖于“等效检查器”来确定输出设计在行为上与输入设计保持相等。商业上广泛使用的对等检查工具包括韵律公司的Conformal equivalence Checker、西门子公司的FormalPro-LEC和Synopsys公司的formal equivalence Checking。所有这些工具都必须是可信的，这意味着如果它们犯了一个错误，并声称，例如，两个设计是等同的，而实际上它们不是，那么最终的硬件可能包含一个错误。而硬件上的漏洞纠正起来可能会非常昂贵。项目的目标。我们打算确定这些等价检查器是否实际上是可信的。它们是否包含破坏它们生成的硬件设计可靠性的bug ？如果是这样的话，我们能否设计出测试或验证技术，使等价检查器更值得信赖？方法。我们将为等效检查器设计新的测试技术。这可能是基于大量随机硬件设计的生成，以及对这些设计的随机突变的应用，以便获得不完全等同的硬件设计对的语料库，这些硬件设计对可以提供给测试中的等效检查器。创新将需要设计随机生成技术和随机突变技术，这些技术倾向于暴露漏洞（如果它们存在），而不会产生过于庞大（因此合成缓慢）的硬件设计。与epsrc研究领域保持一致。该项目与EPSRC的“安全可靠的信息通信技术”优先级保持一致，力求使硬件合成过程更不容易出错。在验证更高抽象层次设计的正确性方面，我们做了很多工作；这个项目通过检查当设计被输入到链中的最后一个“环节”：合成工具时，这些正确性保证不会被破坏，从而补充了这些工作。该项目还涉及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.