BTOR2

Concept

BTOR2 is a word-level intermediate language for hardware model checking that generalizes the bit-level AIGER format with word-level data types, registers, and memories. It is widely used as a backend output by synthesis tools such as Yosys and as an interchange and target format for hardware model checkers, though its reliance on fixed-width bit-vectors limits its ability to express theories such as integer and real arithmetic.

First seen 7/6/2026

Last seen 7/6/2026

Evidence 1 chunks

Wiki v1

WIKI

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.

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

1 connections

Yosys ← uses 100% 1e

Yosys can produce BTOR2 output format.

LINKED ENTITIES

1 links

Yosys USES Extracted graph relationship

CITATIONS

5 sources

5 citations — click to expand

[1] BTOR2 is a word-level generalization of AIGER and provides word-level data types, registers, and memories. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections

[2] Yosys can transform a hardware design description into BTOR2 alongside AIGER, SMV, and SMT-LIB. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections

[3] BTOR2 is a lower-level intermediate language for hardware verification that translation-based model checkers target from higher-level languages such as MoXI. MoXIchecker: An Extensible Model Checker for MoXI

[4] BTOR2 uses bit-vectors of fixed lengths and cannot precisely express theories such as integer or real arithmetic, limiting translation-based model checking approaches. MoXIchecker: An Extensible Model Checker for MoXI

[5] BTOR2 is one of the standard benchmark formats (alongside AIGER) emitted by hardware model checking benchmark generators such as EvolveGen. EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning