bit_accelerator/IMPLEMENTATION_REPORT.md

bit_accelerator_v2 - Verified Status

Everything below was measured by running make test (Verilator 5.020, Icarus Verilog 12.0, Why3 1.6.0 with Z3 4.8.12).

Result

• Simulation: checks=182 fails=0 under both Verilator and Icarus.
• Lint: verilator --lint-only -Wall clean.
• Formal: 33/33 Why3 goals valid with Z3.

Observed cycle timing (1-cycle-latency memory, no stalls)

a = cycle in which op_valid && op_ready is sampled.

Op	Timeline
BIT_GET	READ_REQUEST a+1, READ_RESPONSE a+2, RESULT_VALID a+3 (one cycle)
SET/CLEAR/TOGGLE	READ_REQUEST a+1, READ_RESPONSE a+2, MODIFY a+3, WRITE accepted a+4, RESULT_VALID a+6
Write stalled (mem_ready=0 a+4..a+6)	request and wdata held, accepted a+7, RESULT_VALID a+9
Read stalled (mem_ready=0 a+1..a+2)	accepted a+3, response a+4, RESULT_VALID a+5

Covered by the testbench

• Result value for GET (set/clear bits, cross-word offsets, non-zero base).
• Memory contents after SET/CLEAR/TOGGLE, including word 1 targets.
• Exactly one result_valid pulse per op; op_ready low while busy.
• Write and read backpressure: signals held stable, no early result, write committed once.
• Reset asserted in each of READ_REQUEST, READ_WAIT, MODIFY, WRITE_REQUEST, WRITE_WAIT: no result_valid, no write after reset, DUT idle, and a fresh op completes normally.

Defects found by simulation and fixed

1. result_valid was registered, so it appeared one cycle later than specified (a+4 instead of a+3). It is now combinational from ST_RESULT.
2. A reset in the same cycle as a write handshake let the memory commit the write. mem_valid/mem_write/mem_wstrb/mem_wdata are now forced low while reset is asserted.
3. error was set on any mem_fault; it is now cleared on accept and set only in ST_READ_WAIT.
4. Read-fault tests were added (GET/SET/TOGGLE): error is high in the result cycle, no write is issued, and the next operation clears it. The testbench now exits non-zero on failure.
5. Lint fixes: explicit zero-extension of mem_addr, bit extraction reads read_word[bit_index] directly.
6. The previous testbench did not compile, sampled after the clock edge (racy), and modeled 2-cycle read latency. It was rewritten to log pre-edge values per cycle.

Not verified / known limits

• Only read faults exist; there is no write-fault input path.
• BIT_TEST (3'b001) behaves like GET; no flag output exists.
• base_address << 3 truncates the top 3 bits of base_address, and mem_addr is 61 significant bits.
• The Why3 proofs cover the specification; RTL-to-specification agreement is checked by simulation only.
• Undefined opcodes (101-111) execute as a read with no write and no error.
• No synthesis was run; area/power/frequency numbers elsewhere in this repo are estimates.