Skip to content
STIMSMITH

Bitvector Theory

Concept WIKI v1 · 6/8/2026

In the context of satisfiability modulo theories (SMT), the bitvector theory is a standard SMT-LIB theory used to model fixed-width bit-vector values and operations. It is the formal semantics layer that hardware description tools such as the hwtypes library align with, and it is the theory under which tools like Boolector solve queries about hardware RTL and instruction selection rewrite rules.

Bitvector Theory (SMT-LIB)

The bitvector theory is one of the standard theories supported by SMT solvers, alongside arrays, integer and floating-point arithmetic, uninterpreted functions, and algebraic data types. In an SMT formulation, a theory T assigns meaning to theory-specific symbols by fixing a class of allowable interpretations. The satisfiability problem for bitvector logic then asks, for a given formula, whether it is satisfied by some bitvector interpretation (T-satisfiable), by none (T-unsatisfiable), or by all (T-valid) [1].

Core notation

The notation used in SMT formulations of bitvector logic is summarized in Table I of the source paper and includes the following [1]:

  • BV[n] — the sort for bitvectors of length n (e.g., BV[8] denotes 8-bit bitvectors).
  • +[n], −[n], ×[n], ÷[n] — arithmetic operations performed modulo 2^n.
  • x ++ y — bitvector concatenation of x and y.
  • x[msb : lsb] — bitvector extraction over the indicated bit range.
  • ite(c, x, y) — an if-then-else operator with the same meaning as x in an interpretation I where I ⊨ c, and y otherwise.

The sort BV[8] is used explicitly in the paper's running example, where an architecture Arch is modeled as a term taking bitvector inputs and producing a bitvector output through nested ite expressions [1].

Role in hardware verification and synthesis

Bitvector theory is the semantic backbone for formal reasoning about fixed-width hardware. The hwtypes Python library, which is the formal-analysis companion of the Magma hardware description language, is explicitly described as having semantics that match those of the SMT-LIB theory of bitvectors [2]. This alignment allows circuits written in Magma to be encoded directly as SMT formulas over bitvectors by tracing the inputs of a circuit and the outputs of its architectural state to the outputs of the circuit and the inputs of its architectural state [2].

Solvers and tooling

Boolector is used as the SMT solver for bitvector (and related) queries in the source work [2]. Intermediate representations (IRs) are specified directly in SMT using the pysmt library, and the synthesized rewrite-rule synthesis tool relies on the bitvector theory to determine both the existence of rewrite rules (UNSAT results, indicating no valid rewrite) and the construction of concrete rules (SAT results) [2].

Practical use: instruction selection rewrite rules

The theory is used to encode the problem of synthesizing instruction selection rewrite rules from RTL: an IR operation expressed in bitvector logic is checked for equivalence with an architectural RTL also modeled in bitvector logic, and the SMT solver returns a rule (or proves that none exists) [3]. The paper reports synthesizing rewrite rules for 16-bit processing elements and for the RISC-V ISA, including extensions with floating-point operations expressed in the bitvector sort, in seconds; multi-instruction sequences for pseudo-operations take at most 90 seconds [1] [3].

Related concepts

  • SMT (Satisfiability Modulo Theories) — the general framework under which the bitvector theory is solved.
  • SMT-LIB — the standard language/theory specification that defines the bitvector theory's syntax and semantics.
  • hwtypes — a Python library whose semantics are aligned with the SMT-LIB theory of bitvectors and which is used in conjunction with the Magma HDL.
  • Boolector — an SMT solver used in the source work for bitvector queries.

LINKED ENTITIES

2 links
Synthesizing Instruction Selection Rewrite Rules from RTL using SMT USES
hwtypes IMPLEMENTS

CITATIONS

8 sources
8 citations
[1] Bitvectors are one of the standard theories supported by SMT solvers, alongside arrays, integer and floating-point arithmetic, uninterpreted functions, and algebraic data types. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[2] BV[n] denotes the sort for bitvectors of length n, and +[n], −[n], ×[n], ÷[n] denote arithmetic modulo 2^n. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[3] Bitvector concatenation (x ++ y) and extraction (x[msb:lsb]) are part of the SMT bitvector theory notation. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[4] The hwtypes library has first-class support for formal analysis through its associated Magma HDL, with semantics that match those of the SMT-LIB theory of bitvectors. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[5] An SMT formula is constructed for an architecture by tracing circuit inputs and the outputs of architectural state to the outputs of the circuit and the inputs of its architectural state. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[6] Boolector is used as the SMT solver for the rewrite-rule synthesis problem. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[7] A running example architecture in the paper is modeled as a BV[8] term with nested ite expressions mapping an opcode `inst` to operations such as `y1 −[8] y2` and `y1 +[8] y2`. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT
[8] Rewrite rules for CoreIR operations to 16-bit CGRA processing elements can be synthesized, and for the RISC-V ISA (including floating-point extensions) in seconds, with multi-instruction pseudo-operation sequences taking at most 90 seconds. Synthesizing Instruction Selection Rewrite Rules from RTL using SMT