Scholarlink

<p>Across the broad research field concerned with analyzing computing systems, algorithms and tools revolve around the modeling 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 foundations 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 <span>Btor2C</span>, a translator from word-level sequential circuits in the <span>Btor2</span> language to C&#xa0;programs. We choose the <span>Btor2</span> language as frontend because its simple syntax and bit-precise semantics make it a suitable <i>intermediate representation</i> for analysis purposes. Using <span>Btor2C</span>, we translate <span>Btor2</span> circuits from the Hardware Model Checking Competitions into C programs and analyze them using 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&#xa0;<span>Cbmc</span> (with&#xa0;<span>Btor2C</span> for preprocessing) found more bugs than the best hardware model checkers&#xa0;<span>ABC</span> and&#xa0;<span>AVR</span> in our experiment.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Bridging hardware and software analysis with Btor2C: a word-level-circuit-to-C translator

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年4月30日

查看全文
  • Salih Ates,
  • Dirk Beyer,
  • Po-Chun Chien,
  • Nian-Ze Lee

摘要

Across the broad research field concerned with analyzing computing systems, algorithms and tools revolve around the modeling 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 foundations 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 using 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.