Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict independently. Recently, translating the hardware-modeling language Btor2 to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework Btor2 - Cert to verify safety properties of Btor2 circuits, combining Btor2 -to-C translation, software verifiers, and a new witness validator Btor2 - Val , to answer the above open questions. Btor2 - Cert translates a software violation witness to a Btor2 violation witness; As the Btor2 language lacks a format for correctness witnesses , we encode invariants in software correctness witnesses as Btor2 circuits. The validator Btor2 - Val checks violation witnesses by circuit simulation and correctness witnesses by validation via verification . In our evaluation, Btor2 - Cert successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier Cbmc on translated programs, it uniquely solved, with confirmed witnesses, 8 % of the unsafe tasks for which the hardware verifier ABC failed to detect bugs.
原文链接
分享
引用
