Bitblast Transformation

A bitblast transformation is a technique used in formal verification, particularly in SAT solving and SMT solving. It refers to the process of converting expressions that operate on word-level data types (such as 32-bit integers or bitvectors) into equivalent logic formulas operating on individual bits. This transformation allows complex operations to be handled by Boolean satisfiability solvers (SAT solvers), which operate exclusively on Boolean variables.

Definition

Bitblasting translates word-level variables and operations into purely Boolean logic. For example, a 32-bit integer variable would be decomposed into 32 separate Boolean variables, each representing a single bit.

Process

The bitblast process typically involves the following steps:

1. Bit-level decomposition: Each word-level variable (such as x, a 32-bit integer) is split into individual bits: x₀, x₁, ..., x₃₁.
2. Translation of operations: Word-level operations (such as addition, subtraction, multiplication, and comparisons) are replaced with equivalent bitwise logic circuits. For example:
   1. Addition is replaced by a ripple-carry adder implemented in Boolean logic.
   2. Multiplication is replaced by repeated shifting and addition operations.
   3. Equality checks become a sequence of XOR and NOR operations.
3. Conversion to Boolean formula: The result is a Boolean formula, typically expressed in conjunctive normal form (CNF), which can then be fed directly to a SAT solver.

Applications

Bitblast transformation is widely used in:

• Hardware verification: Formal verification of digital circuits, where bit-level accuracy is required.
• Software verification: Analysis of low-level software (such as embedded systems) where word-level operations must be verified for correctness or safety.
• SMT solving (Bitvector theory): SMT solvers that support bitvectors (such as Z3 and Boolector) rely heavily on bitblasting to reduce bitvector reasoning to pure SAT.
• Symbolic Model Checking: Bitblasting is used to translate transition relations into Boolean logic for SAT-based model checking.

Advantages and Disadvantages

Advantages

• Enables the use of highly optimized SAT solvers for bitvector problems.
• Provides precise handling of bitwise and low-level arithmetic operations.
• Works well for small or medium-sized bitvector problems.

Disadvantages

• Results in a significant blowup in problem size due to the explosion of variables (each bit is a separate Boolean variable).
• Scalability issues for larger word sizes and complex expressions.
• Can be computationally expensive, especially for operations like multiplication on wide bitvectors (e.g., 64-bit or larger).

Bitblast Transformation in emmtrix Studio

emmtrix Studio supports bitblasting through both #pragma directives and the graphical user interface (GUI). The purpose of this transformation is to enable a deeper analysis of how individual bits influence each other. It is particularly useful for the emmtrix Dependency Analyzer, which enables the tool to analyze dependencies between variables at the bit level.

This transformation converts a C function into a boolean representation, breaking down operations into individual bit-level logic. Each supported variable is split into a set of _Bool variables, one for each bit (e.g., _Bool x_bit0, _Bool x_bit1, ...). Unsupported operations are kept as-is, and the original data type is reconstructed.

Unlike traditional bitblasting in SAT solvers, emmtrix Studio applies this transformation selectively to individual functions rather than entire programs. Where necessary (e.g., for function parameters), bit extraction or word reconstruction code is inserted to ensure correctness. Additionally, computationally expensive operations like multiplication or division are not bitblasted to maintain efficiency.

Supported Features

Supported Operations

• Logical and bitwise operations (|, &, ^, ~, &&, ||)
• Shift operations with constant shift amounts (<<, >>)
• Equality comparisons (==, !=)
• Addition and subtraction (+, -)
• Array subscripting
• Implicit and explicit type casts

Supported Data Types

• All integer types
• _Bool
• Arrays

Example

In the following example, bitblasting is applied to an addition of 8-bit integers. The resulting code performs the addition using bitwise logic before passing the computed value to the check function.

void check(unsigned char v) { printf("%02X\n", v); } #pragma EMX_TRANSFORMATION BitBlast void test(unsigned char uc1, unsigned char uc2) { check(uc1 + uc2); }

void test(unsigned char uc1, unsigned char uc2) { _Bool callarg_bit0, ..., callarg_bit7; int tmp, tmp2, ..., tmp24; tmp = (((int)uc1) & 1); tmp2 = (((int)uc2) & 1); callarg_bit0 = (tmp ^ tmp2 ^ (_Bool)0); tmp4 = ((uc1 >> 1) & 1); tmp5 = ((uc2 >> 1) & 1); tmp6 = ((tmp && tmp2) || 0 || 0); callarg_bit1 = (tmp4 ^ tmp5 ^ tmp6); tmp7 = ((uc1 >> 2) & 1); tmp8 = ((uc2 >> 2) & 1); tmp9 = ((tmp4 && tmp5) || (tmp5 && tmp6) || (tmp4 && tmp6)); callarg_bit2 = (tmp7 ^ tmp8 ^ tmp9); tmp10 = ((uc1 >> 3) & 1); tmp11 = ((uc2 >> 3) & 1); tmp12 = ((tmp7 && tmp8) || (tmp8 && tmp9) || (tmp7 && tmp9)); callarg_bit3 = (tmp10 ^ tmp11 ^ tmp12); tmp13 = ((uc1 >> 4) & 1); tmp14 = ((uc2 >> 4) & 1); tmp15 = ((tmp10 && tmp11) || (tmp11 && tmp12) || (tmp10 && tmp12)); callarg_bit4 = (tmp13 ^ tmp14 ^ tmp15); tmp16 = ((uc1 >> 5) & 1); tmp17 = ((uc2 >> 5) & 1); tmp18 = ((tmp13 && tmp14) || (tmp14 && tmp15) || (tmp13 && tmp15)); callarg_bit5 = (tmp16 ^ tmp17 ^ tmp18); tmp19 = ((uc1 >> 6) & 1); tmp20 = ((uc2 >> 6) & 1); tmp21 = ((tmp16 && tmp17) || (tmp17 && tmp18) || (tmp16 && tmp18)); callarg_bit6 = (tmp19 ^ tmp20 ^ tmp21); tmp22 = ((uc1 >> 7) & 1); tmp23 = ((uc2 >> 7) & 1); tmp24 = ((tmp19 && tmp20) || (tmp20 && tmp21) || (tmp19 && tmp21)); callarg_bit7 = (tmp22 ^ tmp23 ^ tmp24); check((unsigned char)((callarg_bit0 << 0) | (callarg_bit1 << 1) | (callarg_bit2 << 2) | (callarg_bit3 << 3) | (callarg_bit4 << 4) | (callarg_bit5 << 5) | (callarg_bit6 << 6) | (callarg_bit7 << 7))); }

Parameters

The following parameters can be configured (each parameter includes its pragma keyword and default value):

Parameter	Default Value	Description
global	false	Transform global variables - Specifies whether global variables should be split into bits. That may result in incorrect code if any global variable is used outside the transformed function.