# Verification Contract

Applies to `rtl/bit_accelerator.sv`.

## Interface

- Reset is synchronous and active-high. Reset cancels any uncompleted operation
  and suppresses its result. `op_ready` is low while `reset` is high.
- An operation is accepted on a cycle with `op_valid && op_ready`. `op_ready`
  stays low until the operation's result pulse.
- A read request completes on `mem_valid && !mem_write && mem_ready`; its data
  completes on `mem_rvalid`. A read fault is signalled with `mem_fault` instead
  of `mem_rvalid`.
- A write request completes on `mem_valid && mem_write && mem_ready`. The cycle
  after the write handshake, `mem_fault` reports a write fault.
- `mem_addr` is `((base_address << 3) + bit_offset) >> 6 << 3` (64-bit
  arithmetic); `mem_wstrb` is all ones.
- `result_valid` is a one-cycle pulse. `error` and `result_bit` are valid in the
  same cycle. On `error`, `result_bit` keeps its previous value.

## Operations

| Opcode | Op | Writes | `result_bit` |
|---|---|---|---|
| 000 | GET | no | bit value |
| 001 | TEST | no | bit value |
| 010 | SET | yes | 1 |
| 011 | CLEAR | yes | 0 |
| 100 | TOGGLE | yes | new bit value |
| 101-111 | undefined | no | `error = 1` |

A read fault ends the operation with `error = 1` and no write. A write fault
reports `error = 1`; whether the memory kept the write is up to the memory.

## Evidence

| Check | Tool | Result |
|---|---|---|
| Lint | `verilator --lint-only -Wall` | clean |
| Simulation | `verification/tb_bit_accelerator.sv`, Icarus 12 and Verilator 5.020 | 0 failures; 23 directed operations, 12 reset-cancellation cases, 2000 random operations per seed with backpressure, read latency 0-3 and fault injection |
| Mutation | 7 hand-made RTL mutants (wrong bit index, wrong address, SET as XOR, ...) | all detected |
| Proofs | `formal/*.mlw`, Why3 1.6 + Z3 4.8.12 | 38/38 goals valid |
| Timing model | `spice/bit_extract.sp`, ngspice 42 | tpd ≈ 94 ps (RC model, not extracted silicon) |
| FPGA wrapper | `fpga/tb/tb_fpga_top.sv` over the UART: RTL (Icarus, Verilator), iCE40 and ECP5 gate-level netlists | 0 failures on each |
| Host tool | `fpga/sim/cosim.sh`: `bitacc selftest` against the RTL through a pseudo-terminal | 2000 operations, 0 mismatches |
| FPGA place-and-route | nextpnr, 5 seeds | iCE40UP5K 39.06 MHz, ECP5-25F 73.22 MHz; both meet board clocks |
| ASIC synthesis | Yosys + ABC on sky130_fd_sc_hd, OpenSTA | 1538 cells, 10,063 µm², netlist proved equal to RTL, 500 MHz pre-layout |

`formal/bit_address.mlw` proves that the RTL's shift/mask datapath equals the
integer address specification when `(base << 3) + offset` does not overflow.
Its trusted base is four facts from the Why3 bit-vector library (listed in the
file), restated because the SMT drivers do not pass them to the solver.
`formal/bit_extract.mlw` proves GET/SET/CLEAR/TOGGLE on 64-bit words change
exactly the target bit.

The proofs are about the datapath expressions; the state machine is checked by
simulation. Random seeds reproduce within one simulator only (Icarus and
Verilator implement `$random` differently).