BTOR2
Overview
BTOR2 is an intermediate representation language for hardware model checking. It is described as a lower-level intermediate language for hardware verification and serves as a standardized format that hardware model checkers can consume directly. It is used both as an interchange format for benchmarks and as the target of translation pipelines from higher-level verification languages.
Relationship to AIGER
BTOR2 is a word-level generalization of the AIGER format. Where AIGER describes hardware systems at the bit level using an and-inverter graph, BTOR2 lifts the representation to the word level by introducing word-level data types together with explicit constructs for registers and memories. This makes BTOR2 a natural target for designs whose natural unit of computation is a word rather than an individual bit.
Tool Support
BTOR2 is supported as one of several backends of the open-source synthesis framework Yosys. Yosys accepts hardware descriptions in hardware description languages such as Verilog, compiles them into its internal RTLIL netlist representation, and can emit the design in AIGER, SMV, BTOR2, or SMT-LIB. Emitting BTOR2 from Yosys enables hardware designs to flow into word-level model checking flows.
Role in Hardware Model Checking
BTOR2 is used both as a benchmark interchange format and as a native input format for hardware model checkers. Benchmark generation frameworks such as EvolveGen, which combine reinforcement learning with high-level synthesis, produce hardware model checking instances in standard formats including AIGER and BTOR2 so that state-of-the-art model checkers can be evaluated on them. The format also enables solver-runtime-guided generation of small-but-hard instances that expose solver-specific weaknesses.
Relationship to Higher-Level Verification Languages
BTOR2 is targeted by translation from higher-level intermediate verification languages. The MoXI intermediate verification language, introduced to standardize symbolic model checking, includes a translator from MoXI to Btor2 in its tool suite. Translation-based model checkers built on top of MoXI dispatch the translated tasks to mature hardware model checkers that consume Btor2.
Limitations
Because BTOR2 is built on bit-vectors of fixed widths, verification tasks that involve more complex theories — such as integer or real arithmetic — cannot be precisely expressed in it. This restricts the extensibility of translation-based model checkers whose source languages include such theories and has motivated verification approaches that operate directly on higher-level languages rather than translating them down to Btor2.