130 billion cases. Then a proof.

Verification mirrors the hierarchy on the schematic and on lot 07 copper: prove the programmable 1-bit LUT cell, compose it into 8-bit slices, then close the full 32-bit export. Digital .dig is the logic source; read-only netlists land in verification/rtl/. Re-export, re-run sign-off.

The property under test is always the same family: out = f(a,b,c) + g(a,b,c) + h(c_in). Two independent 8:1 mux planes per bit feed a ripple carry-select adder. Formal proofs the LUT relations and combinatorial output; directed replay checks the exported netlist against Digital’s vectors; UVM scoreboards the sequential flag path; the gauntlet hammers the FPGA copy of the running machine.

Digital-export sign-off

The main harness in verification/ signs off the Digital-export ALU — not the full CPU, ISA ROM, or memory system. From the repo root, make test runs the fast path.

1. 01 · Formal

   SymbiYosys · 1b → 8b → 32b

   1b: k-induction proves MUX_OUT = OPCODE[{C,B,A}], plus generate/propagate for every input. 8b: same relations per bit-slice. 32b spot: 12 fast regression properties. 32b equiv: Out === golden(...) for all inputs (~74 s). Flags: cover mode for FLAG_WE reachability.

   Inventory: 19 source asserts + 20 cover points (40 + 48 elaborated on 8b). See verification/formal/PROPERTY_INVENTORY.md.

2. 02 · Directed

   476 vectors · Icarus · Digital replay

   Every vector extracted from Digital testbenches passes against the unified golden — no skips. Six flag-only vectors with exp=x are skipped at codegen. Exercises all csel modes and opcode pairs the schematic actually runs.

3. 03 · UVM

   Questa scoreboard · 1b / 8b / 32b

   1b exhaustive: 128-row 0x96 table + 256× LUT sweep + G/P corners. 8b full: CLA boundaries, logic sweep, 5000 random. 32b regression: 476 directed + 91-op coverage + edge cases + flag test + 10k random. Requires Questa (vlog/vsim) — not wired in GitHub Actions yet.

4. 04 · Lint

   Verilator · all three slices

   make lint on 1b, 8b, and 32b exports — zero errors before directed replay runs.

FPGA gauntlet · 10B + 130B

Separate tree: verification/gauntlet/ holds a copy of hardware/fpga/core/rtl/alu.v — the ALU that runs Tomato OS on the Nexys A7. Refresh with make sync; do not edit core from here.

SymbiYosys proves 1b, 8b, and 32b Out ≡ golden. Verilator drives 10,000,000,000 vectors on the 8-bit slice and 130,000,000,000 on the full 32-bit ALU. Directed warmup (LUT×minterm×cin on 8b; low-byte grid on 32b), then random fill. Measured on Apple Silicon: ~25 Mvec/s (8b), ~13–16 Mvec/s (32b) — about 7 minutes for 10B and 2 hours 45 minutes for the recorded 130B run.

Run it yourself

Dependencies for sign-off: python3, yosys, symbiyosys (sby), z3, iverilog, verilator. Gauntlet needs the FPGA OSS CAD Suite on PATH.

cd verification
make signoff              # fast CI (~35 s)
make signoff_full         # + 32b equiv (~3 min)

cd verification/gauntlet
make sync && make claim   # formal + 10B + 130B

Scope & honest limits