Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers

Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee, and Nils Sirrenberg

This work is accepted at TACAS 2024. A preprint and the publisher's version of this article are available for you to download.

Abstract

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.

Reproduction Information

A reproduction package of this work is available on Zenodo (DOI). A previous version of the reproduction package was reviewed by the Artifact Evaluation Committee at TACAS 2024 and awarded the (Functional and) Reusable and Available badges, and won the Distinguished Artifact Award. The updated version fixes some issues in the translator for correctness witnesses.

reusable-badge   available-badge

Tool Information

The source code of the proposed hardware-verification framework Btor2-Cert can be found in this Git repository.

Discovered Issues of Software Verifiers

Verifier Issue description More information
CPAchecker Some bit-vector operations are not supported during translation of
invariants from internal representation back to C		 Issue #1186
Ultimate
Automizer		 Related fixes
Loop invariants in correctness witnesses refer to out-of-bound variables Issue #660
ESBMC Duplicate node IDs in GraphML violation witnesses Issue #1621
CBMC Different error path reported in CBMC's console log and GraphML witness issue #70

Experimental Results

The experimental results reported in the paper can be viewed in the interactive tables below. You can click on the cells in the status columns to see the respective log output and use the respective tabs to show various plots.