# 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)

```systemverilog
// 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`.

```bash
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:

1. Address decomposition: `addr = word * 64 + bit`, `0 <= bit < 64`, and (word, bit) determines the address.
2. Boundaries: offset 64 reaches the next word; offsets 0-63 stay in one word **when the base is word-aligned** (`base mod 8 = 0`).
3. Bit operations: GET returns 0 or 1 and is deterministic; GET after SET/CLEAR returns 1/0.
4. 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:

1. **Correctness**: Formal verification, not testing alone
2. **Determinism**: No undefined behavior, no race conditions
3. **Simplicity**: Minimal instruction set, orthogonal operations
4. **Performance**: Single-digit cycle latency on hits
5. **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