bitvector theory

Concept

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.

First seen 6/8/2026

Last seen 6/8/2026

Evidence 3 chunks

Wiki v1

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

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

explore full graph →

RELATIONSHIPS

2 connections

Synthesizing Instruction Selection Rewrite Rules from RTL using SMT ← uses 100% 1e

The paper uses the SMT-LIB theory of bitvectors for formal analysis.

hwtypes ← implements 100% 1e

hwtypes library semantics match those of the SMT-LIB theory of bitvectors.

LINKED ENTITIES

2 links

Synthesizing Instruction Selection Rewrite Rules from RTL using SMT USES Extracted graph relationship

hwtypes IMPLEMENTS Extracted graph relationship

CITATIONS

8 sources

8 citations — click to expand

[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