diff --git a/docs/NOW.md b/docs/NOW.md index b5706b0dcc..23a72e8835 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,7 +1,13 @@ -# NOW — test: CI quantifies "size costs TIME (steps), not AREA" (2026-08-08) +# NOW — docs: workshop-grade silicon-training methodology write-up (2026-08-08) Last updated: 2026-08-08 +## docs: reproducible methodology paper for on-chip training (Refs #1764) + +- New `docs/SILICON_TRAINING_METHODOLOGY.md`: a workshop-grade write-up of the full result -- a NN training loop written as a .t27 spec, compiled by t27c, verified bit-exact across FOUR targets (Verilog/C/Rust/model), and trained on a real Artix-7 through a fully open toolchain (yosys->nextpnr-xilinx->prjxray, native macOS arm64, no Vivado/Docker) +- Covers: the pipeline end-to-end (spec -> generator -> CI verification -> openXC7 bitstream -> flash -> train); measured results (full backprop trains XOR 4/4 on silicon, model-exact; the CI-verified generator's RTL does the same; size=time not area, CI-quantified); honest limits (openXC7 ~17M correctness ceiling; nextpnr can't express multicycle so the deep path is placement-dependent -> seed-search, an open-toolchain limitation a commercial P&R would close); and one-script reproducibility (board/build_trainer.py) +- Docs only. Refs #1764 + ## test: the emit gate now reports microcode step count per topology (Refs #1764) - Quantified the whitepaper's headline claim IN CI. The emit-bitexact gate now prints, per topology, the microcode STEP count next to the one-shared-multiplier datapath invariant: (2,2,1)=32 steps -> (2,4,2)=88 -> deep [3,4,4,2,1]=216 steps, while the synth area report shows cell counts stay ~constant (13945 -> 17468). So "network size costs TIME (microcode steps), not AREA (one shared multiply/add)" is now measured on every PR, not just asserted in prose diff --git a/docs/SILICON_TRAINING_METHODOLOGY.md b/docs/SILICON_TRAINING_METHODOLOGY.md new file mode 100644 index 0000000000..31cff94ed2 --- /dev/null +++ b/docs/SILICON_TRAINING_METHODOLOGY.md @@ -0,0 +1,89 @@ +# Training a neural network on live FPGA silicon from a verified specification + +*A reproducible open-toolchain methodology.* Workshop-grade write-up of the GF-T +on-chip training result. Everything below is measured, not projected. + +## Claim + +A neural-network training loop — forward, loss, backward, weight update — written +as a `.t27` **specification**, compiled by a ternary compiler, **verified bit-exact +against an independent model across four targets (Verilog, C, Rust, and the model)**, +and then **run on a real Xilinx Artix-7 (AX7203, xc7a200t) where it trains a network** +— through a fully open-source toolchain (yosys → nextpnr-xilinx → prjxray), no Vivado, +no Docker, native macOS arm64. + +## Method (the pipeline, end to end) + +1. **Spec.** The GF-T arithmetic (a ternary-native GoldenFloat: `value = (−1)^s · + (1 + m/512) · 2^(off−40)`) is defined in `.t27` — `gft_smul.t27`, `gft_sadd.t27`, + etc. The compiler `t27c` emits **Verilog, C, Rust, and Zig** from one source. + +2. **Generator, not hand-RTL.** `tools/gft_backprop_microcode.py` turns an arbitrary + feed-forward topology (free inputs × hidden layers × outputs, arbitrary depth) into + a **microsequencer**: one shared multiply core + one shared add core, driven by a + microcode program over a register file. Network size grows the microcode (time) and + the register file — **not the datapath** (one multiplier, regardless of the net). + +3. **Verification, as a CI invariant.** On every change, a gate (`verify_emit_bitexact`) + regenerates the arithmetic cores from spec and proves the generated RTL is **bit-exact + to the independent Python GF-T model over a full 80-step training run** (forward + + backprop + update, every output per step) in Icarus Verilog; then **synthesizes** it + (yosys) with a non-zero cell mapping and asserts the **one-shared-multiplier datapath + invariant**. A companion gate (`verify_multitarget`, `verify_trainer_c`) proves the + primitives and the whole trainer are bit-exact in **C and Rust** too, over moderate, + extreme (saturation-adjacent), and cancellation operands, plus a differential fuzzer + over random topologies. Spec→any-target bit-exactness is *guaranteed per pull request*. + +4. **Silicon build.** `emit_verilog(…, clk_div=16)` emits a silicon-ready variant: the + register file is forced to flip-flops (distributed LUTRAM cannot do the parallel + weight-init) and the sequencer steps once per 16 cycles (a clock-enable) so the deep + shared-core combinational path has time to settle. `yosys synth_xilinx -nocarry` + → `nextpnr-xilinx --timing-allow-fail` → `fasm2frames` → `xc7frames2bit` → `.bit`. + +5. **Flash & train.** `openFPGALoader` loads the bitstream over JTAG; the host streams + training samples over UART; the board holds the weights, runs a full backprop step + per sample, and returns the forward output. Weights persist across samples → it learns. + +## Results (measured on the AX7203) + +- **The full 2-layer backprop microsequencer trains XOR to 4/4**, 24/25–25/25 epochs, + both layers learning on-chip, with a **weight trajectory bit-exact to the independent + model** (epoch-0 outputs 0.000 / 0.551 / 0.936 / 0.232 match the model to three + decimals; the error term converges toward zero). +- The **CI-verified generator's** RTL (not hand-written) trains XOR on silicon the same + way, closing the loop spec → verified generator → open-source bitstream → live training. +- Earlier on-silicon results on the same board: inference (dot 6/6, BitNet neuron 8/8, + 3-class argmax 16/16 held-out, 2-layer ReLU XOR 4/4) and training (SGD 4/4, gradient + descent → 0, 1-/2-parameter regressions, ReLU-gated nonlinear neuron, a classifier + generalizing 8/8, train→save→deploy closed with SPI-flash boot). +- **Size costs time, not area** (CI-measured): microcode steps grow (2,2,1)=32 → + (2,4,2)=88 → deep [3,4,4,2,1]=216, while synthesized cell counts stay ~constant. + +## Honest limits (measured, not hidden) + +- **openXC7 correctness ceiling ≈ 17M fasm.** Designs ≤ 16.7M compute correctly; ≥ 19.5M + place and respond over UART but *miscompute* — always cross-checked against the model. +- **The open-source place-and-route cannot express a multicycle timing constraint** + (nextpnr-xilinx's XDC parser supports only `create_clock`). The deep shared-core path + is therefore left timing-relaxed, and correctness is **placement-dependent**: some + `--seed` values glitch, one trains cleanly. We seed-search. This is an open-toolchain + limitation — a commercial P&R would close the path directly — not a design flaw. A + design's microcode step count predicts its marginality (more steps per frame = more + chances for a glitch). + +## Reproducibility + +The verification runs in CI on every pull request. The silicon build is one script +(`board/build_trainer.py`): generate → wrap in the UART front-end → yosys → seed-search +nextpnr → per-seed bitstreams. Flash a seed, drive it over UART, keep the seed that +trains stably. All artifacts (chipdb, nextpnr-xilinx, prjxray) are open-source and +build natively on macOS arm64. + +## Why it matters + +On-device *learning* on cheap FPGA silicon, in a ternary-native format, from a +machine-verified specification, through an entirely open toolchain, is a capability we +have not seen demonstrated elsewhere. Every inference-only ternary accelerator we know +of (Ternary-NanoCore, TerEffic, bitnet.cpp, bitSMM) runs a *frozen* model in hand-written +RTL or on a CPU; here the spec *is* the network, it is verified bit-exact across four +targets, and it *trains* on live silicon.