Bit-String Hardware Accelerator

A dedicated hardware accelerator for bit-string operations with formal verification.

Architecture Overview

request (base_address + bit_offset)
    ↓
STAGE 1: Address Generator (base + offset)
    ↓
STAGE 2: Word & Bit Index Calculator (÷64, mod 64)
    ↓
STAGE 3: Memory Access (TLB → L1 Cache)
    ↓
STAGE 4: Bit Extraction (barrel shifter + AND)
    ↓
STAGE 5: Writeback (register result)
    ↓
result (0 or 1)

Supported Operations

BIT_GET (0b000): Read single bit value
BIT_TEST (0b001): Test bit and set condition flag
BIT_SET (0b010): Set single bit to 1 (read-modify-write)
BIT_CLEAR (0b011): Clear single bit to 0 (read-modify-write)
BIT_TOGGLE (0b100): Toggle single bit (read-modify-write)

Design versions

Version	Files	Status
v2	`rtl/bit_accelerator_v2.sv`	Verified design. Lint-clean (`verilator -Wall`), 182 testbench checks pass under Verilator and Icarus.
v1	`rtl/bit_accelerator.sv` + submodules	Reference only, not built. `result_valid`/`result_bit` are driven from two processes, and its testbench does not compile.

Interface (v2)

// Operation interface
input  logic        op_valid;       output logic op_ready;
input  logic [63:0] base_address;   // byte address
input  logic [63:0] bit_offset;     // bit offset from base
input  logic [2:0]  operation;      // 000 GET, 001 TEST, 010 SET, 011 CLEAR, 100 TOGGLE
output logic        result_valid;   // one-cycle pulse
output logic        result_bit;     // valid with result_valid
output logic        error;          // set by a read fault, valid with result_valid,
                                    // held until the next operation is accepted
// Memory interface (valid/ready)
output logic        mem_valid, mem_write;
output logic [63:0] mem_addr;       // 8-byte-aligned byte address
output logic [63:0] mem_wdata;      output logic [7:0] mem_wstrb;
input  logic        mem_ready, mem_rvalid, mem_fault;
input  logic [63:0] mem_rdata;

Opcodes 101-111 are undefined; v2 executes them as a read with no write. Write faults are not modelled.

Address calculation

absolute_bit = (base_address * 8) + bit_offset    (mod 2^64)
word_address = absolute_bit / 64
bit_index    = absolute_bit mod 64
result       = (memory[word_address] >> bit_index) & 1

Directory structure

bit_accelerator/
├── rtl/bit_accelerator_v2.sv          # verified design
├── rtl/*.sv                           # v1 (reference only)
├── testbenches/tb_bit_accelerator_v2.sv
├── formal/bit_addressing.mlw          # specification + lemmas (Why3)
├── formal/bit_addressing_proofs.mlw   # derived lemmas
├── scripts/prove.sh                   # proves every goal; fails unless all are Valid
├── isa/BIT_ISA.md, docs/DATAPATH.md
├── Makefile, build.sh, run_v2_sim.sh
└── IMPLEMENTATION_REPORT.md           # measured results

Build and verification

Prerequisites (Ubuntu 24.04): apt-get install verilator iverilog why3 z3, then why3 config detect.

make test           # lint + Verilator + Icarus simulation + Why3 proofs
make lint           # verilator --lint-only -Wall on v2
make sim            # v2 testbench under both simulators
make formal         # every Why3 goal must be proved by Z3
make formal-cvc4    # informational cross-check with CVC4
./build.sh          # same as make test, fails if a tool is missing

Formal verification

formal/ is checked by Why3 1.6 with Z3 4.8.12: 33/33 goals valid, no axioms beyond the Why3 standard library. The lemmas cover:

Address decomposition: addr = word * 64 + bit, 0 <= bit < 64, and (word, bit) determines the address.
Boundaries: offset 64 reaches the next word; offsets 0-63 stay in one word when the base is word-aligned (base mod 8 = 0).
Bit operations: GET returns 0 or 1 and is deterministic; GET after SET/CLEAR returns 1/0.
Non-interference: SET or CLEAR on one word does not change a GET from another word.

An earlier draft of these files was not valid Why3 and stated three theorems that are false (bit_63_same_word, bit_index_wraps_at_64 without the alignment condition, and within_word_uniqueness). Z3 proves their negations; they were corrected.

The proofs are about the specification. Agreement between the specification and the RTL is checked by simulation, not proved.

Testing

tb_bit_accelerator_v2.sv is cycle-accurate and self-checking (exits non-zero on any failure). It checks:

GET results (set and clear bits, offset 64, non-zero base) and exact cycle timing
SET/CLEAR/TOGGLE memory contents, including cross-word offsets
one result_valid pulse per operation; op_ready low while busy
read and write backpressure: request and data held stable, write committed once
reset in each of READ_REQUEST, READ_WAIT, MODIFY, WRITE_REQUEST, WRITE_WAIT
read faults on GET/SET/TOGGLE: error in the result cycle, no write, cleared by the next op
undefined opcodes: no write

Hardware estimates

The figures below are design targets, not measured: no synthesis, place-and-route or power analysis has been run.

Scenario	Latency
L1 cache hit	4 cycles
L2 cache miss	10-15 cycles
Memory miss	50+ cycles

Gate count ~50k (7nm), area ~0.6 mm², power ~2.5 mW active, 1+ GHz

Performance Comparison

Traditional LOAD-SHIFT-AND Sequence

LOAD  r1, [base]         (3-50 cycles: cache/memory)
SHIFT r1, r1, offset     (1 cycle)
AND   r1, r1, 1          (1 cycle)
TOTAL: 5-52 cycles

Dedicated BIT_GET Instruction

BIT_GET r1, base, offset (4-15 cycles: includes memory)
TOTAL: 4-15 cycles
IMPROVEMENT: 20-80% latency reduction

Limitations & Future Work

Current Scope

64-bit word size (fixed)
Single-bit operations only (no multi-bit extract yet)
No atomic multiword operations
No GPU integration

Future Extensions

Variable-width field extraction
Atomic compare-and-swap for multiword fields
SIMD bit-parallel operations
Hardware-assisted population count pipeline

Design Philosophy

This accelerator prioritizes:

Correctness: Formal verification, not testing alone
Determinism: No undefined behavior, no race conditions
Simplicity: Minimal instruction set, orthogonal operations
Performance: Single-digit cycle latency on hits
Verification: Machine-checkable proofs, not documentation

References

Intel 64 & IA-32 Architecture

Bit Manipulation Instructions (BMI, BMI2)
BITFIELD, BIT_SET, BIT_CLEAR semantics

Hardware Design

Kogge-Stone parallel-prefix adder (address gen)
Logarithmic barrel shifter (bit extraction)
Standard pipelined memory interface

Formal Methods

Why3 platform for machine verification
Euclidean division properties
Non-interference proofs for memory operations