Abstract

Across the broad research field concerned with analyzing computing systems, algorithms and tools revolve around the model languages used to describe the systems, hindering their applications to similar problems of systems in other modeling languages. For example, the research communities for formal verification and testing of hardware and software share common theoretical foundation and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it demands effort for one community to enjoy the advancements of the other, as analyzers assume different modeling languages for input instances. To bridge the gap between hardware and software analysis, we propose Btor2C, a translator from word-level sequential circuits in the Btor2 language to C programs. We choose the Btor2 language as frontend because its simple syntax and bit-precise semantics make it a suitable intermediate representation for analysis purposes. Using Btor2C, we translate Btor2 circuits from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Intl. Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware model checkers for enhanced quality assurance: Prominently, the software verifier CBMC (with Btor2C for preprocessing) found more bugs than the best hardware model checkers ABC and AVR in our experiment.

Reproduction Information

The Git repository contains the version of Btor2C used in the evaluation. The benchmark set used in the evaluation can be downloaded from this repository.