Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator
This work is accepted at TACAS 2023.
A 
preprint and the 
publisher's version of this article are available for you to download.
Abstract
Across the broad field for the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such situation is the studies on formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a translator from word-level sequential circuits to C programs. We choose the Btor2 language as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the C language, supported by most static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance.
Reproduction Information
A reproduction package of this work is available on Zenodo
(
).
A previous version of the reproduction package was reviewed by the Artifact Evaluation Committee at TACAS 2023 and awarded the (Functional and) Reusable and Available badges.
The updated version fixes the issues found by the reviewers.
The 
Git repository contains the revision of Btor2C used in the evaluation. The benchmark set used in the evaluation can be downloaded from this repository.
Full Results
This table contains the results of all hardware and software verifiers evaluated in the paper. 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.