Mirrored from https://github.com/SNAPKITTYAGENT9NOVA/bit-string-accelerator at commit d2b5cfe. Part of the SnapKitty October 2026 main drop.

bit-string-accelerator

Synthesizable SystemVerilog bit-string accelerator for deterministic 64-bit-word bit addressing.

effective_bit_address = (base_address * 8) + bit_offset     (mod 2^64)
word_address          = (effective_bit_address / 64) * 8
bit_index             = effective_bit_address mod 64

Operations: GET, TEST, SET, CLEAR, TOGGLE. Interface contract and verification evidence: docs/verification.md.

Layout

Path	Contents
rtl/, verification/, formal/, isa/, spice/, docs/	Compact accelerator, its self-checking testbench, Why3 proofs, ISA and timing model
bit_accelerator/	Multi-stage v2 accelerator with its own testbench and proofs (also in rust-opencl-gpu)
fpga/	Hardware build: UART + block-RAM wrapper, iCEBreaker and ULX3S bitstreams, host tool bitacc (fpga/README.md)
asic/	sky130 standard-cell synthesis, equivalence proof, timing (asic/README.md)
pcie/	Parallel engine with range operations (count, find, fill, bulk logic, pattern match) + PCIe core for the LiteFury, LiteX SoC, host program, open-source timing flow (pcie/README.md)
tapeout/	Tiny Tapeout (ttsky26d, sky130A) project, hardened and prechecked (tapeout/README.md, tapeout/SIGNOFF.md)
gpu/	Rust/OpenCL (ocl) crate from rust-opencl-gpu
.github/workflows/ci.yml	CI: lint, simulation, proofs, SPICE, Rust

Requirements

Ubuntu 24.04:

sudo apt-get install iverilog verilator why3 z3 ngspice pocl-opencl-icd ocl-icd-opencl-dev \
  yosys nextpnr-ice40 nextpnr-ecp5 fpga-icestorm fpga-trellis
why3 config detect

plus a Rust toolchain (1.85 or newer) for gpu/. pocl-opencl-icd provides a CPU OpenCL device; any other OpenCL driver works too.

Build and test

make test          # everything CI runs
make lint          # verilator -Wall
make sim           # testbench under Icarus and Verilator (SEED=n OPS=n to vary)
make formal        # Why3 proofs, every goal must be proved by Z3
make spice         # ngspice timing model
make accel         # bit_accelerator/ v2: lint, sim, proofs
make gpu           # gpu/: cargo fmt, clippy, tests
make fpga          # FPGA wrapper: lint, testbench, host co-simulation, both bitstreams
make fpga-gl       # FPGA wrapper on post-synthesis netlists (slow)
make asic          # sky130 synthesis + RTL/netlist equivalence proof
make pcie          # parallel engine + PCIe core vs the reference core (make -j helps)
make tapeout       # Tiny Tapeout project: RTL test at both divisor settings

Roadmap

Single-op core (reference, proofs) → parallel engine (pcie/, identical results) → DMA work queue → range operations (one descriptor, up to the whole bit store) → LiteFury PCIe prototype → custom PCIe board, with the Tiny Tapeout chip (tapeout/) as a separate silicon proof of the core. The PCIe design does not depend on the transport, so the same card works in the NUC's M.2 slot or in a USB4/Thunderbolt enclosure.

Running on hardware

make -C fpga icebreaker prog-icebreaker (or ulx3s prog-ulx3s) builds and loads a bitstream. Then bitacc --port /dev/ttyUSB1 selftest runs the on-board acceptance test. See fpga/README.md.

Target	Size	Speed
iCE40UP5K (iCEBreaker), core + UART + RAM	1138 LC (21%), 4 BRAM	39.06 MHz (12 MHz board clock)
ECP5 25F (ULX3S), core + UART + RAM	1171 LUT4 (4%), 2 BRAM	73.22 MHz (25 MHz board clock)
sky130 HD standard cells, core only	1538 cells, 10,063 µm²	500 MHz pre-layout, typical corner

GPU tests run serially (RUST_TEST_THREADS=1): PoCL 5.0 can abort with a pocl_release_dlhandle_cache assertion when several OpenCL contexts are released from different threads at the same time. With one test thread it passed 40 of 40 runs, against 26 of 40 with parallel threads.

Known limits

• BIT_TEST behaves like BIT_GET; there is no separate condition flag output.
• base_address << 3 drops the top 3 bits of base_address (64-bit wrap).
• The bitstreams have not been run on a physical board yet (no board was available); pin assignments come from the boards' reference constraint files.
• asic/ numbers are pre-layout for the bare core. tapeout/ has a full layout (GDS) of the Tiny Tapeout top that passes DRC, LVS, antenna, timing and the Tiny Tapeout precheck; it has not been submitted or fabricated. The SPICE deck is an RC model, not extracted silicon.
• The PCIe design has not run on a LiteFury: the bitstream needs Vivado. An open-source place and route (nextpnr-xilinx) reaches 88 MHz (84 MHz with a 2-unit MATCH), not 125 MHz; Vivado's result is unknown. The card is slower than one CPU core for COUNT/BULK; MATCH (pattern search) with 2 units is expected to be about 2x a 4-thread CPU at 125 MHz and about 1.2-1.5x at 84 MHz; see pcie/README.md.

The Windows OpenCL SDK and OpenCL.lib from rust-opencl-gpu are not included here; the ocl crate locates the system OpenCL library.

---

License

Licensed under EPL-2.0. Full text: LICENSE.