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