---

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 symbolic encoding, satisfiability solving, and abstraction refinement. Nevertheless, it requires significant effort for one community to benefit from 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.

Experimental Results

Click on the preconfigured links below to view the corresponding tables and figures in the paper.

• Table 1: Applying modulo operations eagerly vs. lazily
• Table 2: Effects of reducing array duplication on (a) 84 handcrafted tasks and (b) 157 benchmark tasks
• Table 3: Summary of the results on bit-vector and array benchmark tasks
• Table 4: Results on blasted array tasks
• Table 5: Results of 22 programs generated by Btor2C and v2c
• Figure 4: Quantile plots for (a) BV proofs, (b) BV alarms, (c) Array proofs, and (d) Array alarms
• Figure 5: Comparing bug-hunting abilities
• Figure 6: Comparing BMC with different backend SMT solvers
• Figure 7: Comparing BMC using different unrolling strategies
• Figure 8: Comparing (a) CPU-time and (b) memory usage of AVR and ESBMC