Every module machine-checked, and the checkers find three bugs the board never showed

Before this

On 2026-07-29 the carry look-ahead block got wired in as the ALU’s adder. It had compiled and had a testbench and nothing instantiated it. The toolchain was inferring the adder from numeric_std and the look-ahead was decorative. It now has a 9-bit carry-out and a sum output, SUB, SBB and CMP feed it two’s complement and invert the carry into the 8008 borrow flag, and an exhaustive testbench sweeps all 656,384 arithmetic cases against a reference model.

What I tried, 08-07

A synth-plugin target using the ghdl-yosys plugin, and a netlist-vhdl target that runs each module through Yosys write_vhdl so the round-tripped netlist can be checked against the RTL. Then, module by module: stack_pointer got PSL properties proven by k-induction under SBY plus a miter against its netlist, and a cocotb random walk that runs against both. state_timing_generator got a full property suite, 21 arcs and the status table, proven by k-induction. machine_cycle_control got bmc and cover. condition_flags k-induction. The ALU’s write_vhdl round trip was proven equivalent by an SBY miter. Combinational modules went through EQY. The instruction decoder got an exhaustive 256-opcode sweep against a Python model written from the datasheet, and that found issue #4.

write_vhdl splits vector flops, which breaks EQY’s partition matching, so sequential modules use SBY miters instead. GitHub Actions runs all of it on push.

What I tried, 08-08

register_file, stack_memory, instruction_register, temp_registers, interrupt_ready_ff and ahl_pointer all got properties and miters. memory_io_control got a 21-scenario cocotb suite. The assembly regression suite joined CI with the AS assembler built from pinned source, which exposed that NUL bytes in the sim log had been blinding GNU grep. ANA, XRA and ORA joined the ALU sweep, now 1,049,600 cases. A READY/WAIT stress test, interrupt jams with NOP, HLT and 3-byte instructions and during WAIT, 14-bit PC wrap, a 48-combination conditional matrix, and composition proofs across the cycle-control and timing-generator cluster.

The verification plan was audited row by row against the spec stack. All 15 open spec questions were ratified and isa.json realigned with the PDFs. Orphan modules and dead fabric were deleted.

What broke

Three RTL bugs, none of which the board had ever shown.

The external cycle code on D6 and D7 was transposed relative to the datasheet’s table, and during H:L data cycles the raw H byte rode the bus where the code belongs. Nothing on the Versa decodes those bits, so silicon never noticed. A period-correct external controller would have. The new cocotb bus-protocol monitor caught it on its first run: 265 violations before the fix, 0 after, across 341 T1 and 341 T2 checks.

The decoder flagged CPr with opcode 0xFF as memory-indirect.

INP wasn’t driving the condition flip-flops onto the bus at PCC T4.

What I measured

Every checker was mutation-tested by planting a bug and confirming it fails. The differential fuzzer generates seeded random legal programs (forward-only jumps, leaf-only calls, terminating by construction) and runs them whole-system on both the RTL and netlist cores under three oracles: the bus monitor, a per-instruction datasheet timing check, and an rtl-vs-netlist trace diff. 20 seeds on both cores, all traces identical, zero violations. A dropped ALU inverter planted in the netlist was caught by the trace diff on 2 of 20 seeds.

Regression suite is 37 programs.

Next

Nothing on the verification side. The README scorecard shows every module with something machine-checked behind it.