From ef769f140052a1bf9ab8ce4bc937cc17cb7057b0 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Fri, 7 Aug 2026 07:04:43 +0700 Subject: [PATCH] feat: GF-T on-chip trainer primitive (forward+grad+update in one step) gft_train1.t27: on_comb(w,x,t,eta) runs one full SGD step of a 1-weight linear neuron combinationally -- forward y=w*x, error e=y-t, gradient g=e*x, update w'=w-eta*g -- reusing the verified smul/sadd/neg/mag* helpers from gft_sgd_step. The on-device training primitive: with the weight in a register, the whole forward+backward+update runs on-chip and the host streams only (x,t) data. Proven on a live AX7203 (uart_train1.v): streaming (x, t=1.5*x) with varying x, the board's weight converges 0.25 -> ~1.42 toward the hidden w*=1.5. In-spec tests 3/3 (learn/optimum/ascend), iverilog bit-exact. docs/NOW.md updated. Refs #1764 Co-Authored-By: Claude Opus 4.8 --- docs/NOW.md | 10 ++- specs/ternary/gft_train1.t27 | 124 +++++++++++++++++++++++++++++++++++ 2 files changed, 133 insertions(+), 1 deletion(-) create mode 100644 specs/ternary/gft_train1.t27 diff --git a/docs/NOW.md b/docs/NOW.md index 7c7700182..1506a85f8 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,7 +1,15 @@ -# NOW — demo: GF-T learns (end-to-end on-device training demo) (2026-08-07) +# NOW — feat: GF-T on-chip trainer primitive (2026-08-07) Last updated: 2026-08-07 +## feat: GF-T on-chip trainer primitive — proven on AX7203 (Refs #1764) + +- **NEW** spec `specs/ternary/gft_train1.t27` — `on_comb(w,x,t,eta)` runs one full SGD step of a 1-weight linear neuron combinationally: forward `y=w*x` → error `e=y-t` → gradient `g=e*x` → update `w'=w-eta*g` (reuses the verified `smul/sadd/neg/mag*` helpers from `gft_sgd_step`) +- `test` block (learn/optimum/ascend) 3/3 PASS via `icarus-simulate` per L4 +- This is the on-device training primitive: with the weight held in a register the whole forward+backward+update runs on-chip; the host streams only `(x,t)` data +- Proven on a live AX7203 (`uart_train1.v`): streaming `(x, t=1.5*x)` with varying x, the board's weight converges 0.25 → ~1.42 toward the hidden `w*=1.5` +- Spec-only; no `gen/`/`coq/` edits; no new `*.sh`; Refs #1764 + ## demo: GF-T learns — end-to-end training proof (Refs #1764) - Branch: `feat/gft-training-demo` (independent of the spec stack — inlines the models) diff --git a/specs/ternary/gft_train1.t27 b/specs/ternary/gft_train1.t27 new file mode 100644 index 000000000..6b69e1591 --- /dev/null +++ b/specs/ternary/gft_train1.t27 @@ -0,0 +1,124 @@ +module GftTrain1; +// #1764 + GF-T: a GF-T SGD weight update -- w' = w - eta * g, the final brick of an +// on-device training step (forward softmax -> loss -> gradient g -> THIS update). +// eta is the (positive) learning rate; g the gradient (signed); w the weight (signed). +// Composes the verified primitives: signed multiply (smul over the RNE magnitude +// mul) + subtract (sadd + neg). Bit-exact to the integer oracle; accuracy is to +// GF-T16 precision (<=1 ULP; ~0.03 abs at the largest magnitudes). +// +// Inputs: w, g, eta signed GF-T16 (u32). Output: updated weight w' GF-T16 (u32). + +fn magadd(a: i32, b: i32) -> i32 { + var ao : i32 = a >> 9; var am : i32 = a & 511; + var bo : i32 = b >> 9; var bm : i32 = b & 511; + var ho : i32 = bo; var hm : i32 = bm; var lo : i32 = ao; var lm : i32 = am; + if (ao >= bo) { ho = ao; hm = am; lo = bo; lm = bm; } + var hs : i32 = 512 + hm; var ls : i32 = 512 + lm; + var d : i32 = ho - lo; if (d > 11) { d = 11; } + var losh : i32 = ls >> d; var rem : i32 = ls - (losh << d); + var s : i32 = hs + losh; var off : i32 = ho; var mant : i32 = s - 512; + if (s >= 1024) { + var g : i32 = s & 1; var pre : i32 = s >> 1; mant = pre - 512; + if (g == 1) { if (rem > 0) { mant = mant + 1; } else { if ((pre & 1) == 1) { mant = mant + 1; } } } + off = ho + 1; if (off >= 80) { off = 80; } + } else { + var t : i32 = rem << 1; var hf : i32 = 1 << d; + if (t > hf) { mant = mant + 1; } else { if (t == hf) { if ((s & 1) == 1) { mant = mant + 1; } } } + } + if (mant >= 512) { mant = 0; off = off + 1; if (off >= 80) { off = 80; } } + return (off << 9) | mant; +} + +fn magsub(hi: i32, lo: i32) -> i32 { + if (hi == lo) { return 0; } + var ho : i32 = hi >> 9; var hm : i32 = hi & 511; + var lo_o : i32 = lo >> 9; var lm : i32 = lo & 511; + var d : i32 = ho - lo_o; var hs : i32 = (512 + hm) << 14; + var la : i32 = 0; var sticky : i32 = 0; + if (d >= 26) { la = 0; sticky = 1; } + else { var ls : i32 = (512 + lm) << 14; la = ls >> d; if ((ls - (la << d)) > 0) { sticky = 1; } } + var diff : i32 = hs - la; var off : i32 = ho; + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + if (diff < 8388608) { if (off > 1) { diff = diff << 1; off = off - 1; } } + var q : i32 = diff >> 14; var rem : i32 = diff - (q << 14); var half : i32 = 8192; var mant : i32 = q - 512; + if (rem > half) { mant = mant + 1; } + else { if (rem == half) { if (sticky == 1) { mant = mant + 1; } else { if ((q & 1) == 1) { mant = mant + 1; } } } } + if (mant >= 512) { mant = 0; off = off + 1; if (off >= 80) { off = 80; } } + return (off << 9) | mant; +} + +fn sadd(a: u32, b: u32) -> u32 { + if (a == 0) { return b; } + if (b == 0) { return a; } + var sa : i32 = (a >> 16) as i32; var ma : i32 = (a & 65535) as i32; + var sb : i32 = (b >> 16) as i32; var mb : i32 = (b & 65535) as i32; + if (sa == sb) { return ((sa << 16) | magadd(ma, mb)) as u32; } + var bsign : i32 = sa; + var r : i32 = magsub(ma, mb); + if (ma < mb) { r = magsub(mb, ma); bsign = sb; } + if (r == 0) { return 0; } + return ((bsign << 16) | r) as u32; +} + +fn neg(v: u32) -> u32 { + if (v == 0) { return 0; } + return v ^ 65536; +} + +fn magmul(a16: i32, b16: i32) -> i32 { + var ao : i32 = a16 >> 9; var am : i32 = a16 & 511; + var bo : i32 = b16 >> 9; var bm : i32 = b16 & 511; + var prod : i32 = (512 + am) * (512 + bm); + var carry : i32 = 0; if (prod >= 524288) { carry = 1; } + var q : i32 = prod >> 9; var r : i32 = prod & 511; var half : i32 = 256; + if (carry == 1) { q = prod >> 10; r = prod & 1023; half = 512; } + var mant : i32 = q - 512; + if (r > half) { mant = mant + 1; } + if (r == half) { if ((q & 1) == 1) { mant = mant + 1; } } + var sm : i32 = ao + bo + carry; + var out_off : i32 = 0; + if (sm >= 40) { var res : i32 = sm - 40; if (res >= 80) { out_off = 80; } else { out_off = res; } } + if (mant >= 512) { mant = 0; out_off = out_off + 1; if (out_off >= 80) { out_off = 80; } } + return (out_off << 9) | mant; +} + +// softmax: p_sel = 2^(l_sel - M) / sum_i 2^(l_i - M), M = max logit. + +// signed GF-T multiply: sign = xor of signs, magnitude = RNE magnitude mul. +fn smul(a: u32, b: u32) -> u32 { + if (a == 0) { return 0; } + if (b == 0) { return 0; } + var sgn : i32 = ((a >> 16) & 1) as i32; + var sb : i32 = ((b >> 16) & 1) as i32; + if (sgn != sb) { sgn = 1; } else { sgn = 0; } + var mag : i32 = magmul((a & 65535) as i32, (b & 65535) as i32); + if (mag == 0) { return 0; } + return ((sgn << 16) | mag) as u32; +} + +// One full on-chip SGD step of a 1-weight linear neuron: +// forward y = w*x ; error e = y - t ; gradient g = e*x ; update w' = w - eta*g. +// The whole forward+backward+update runs on the FPGA; the host streams only (x,t). +fn on_comb(w: u32, x: u32, t: u32, eta: u32) -> u32 { + var y : u32 = smul(w, x); + var e : u32 = sadd(y, neg(t)); + var g : u32 = smul(e, x); + var delta : u32 = smul(eta, g); + return sadd(w, neg(delta)); +} +// w=0.5,x=1.0,t=1.0,eta=0.5 -> y=0.5,e=-0.5,g=-0.5,delta=-0.25,w'=0.75 (20224). +test learn { assert_eq(on_comb(19968, 20480, 20480, 19968), 20224); } +// at optimum w=1.0,x=1.0,t=1.0 -> no change (20480). +test optimum { assert_eq(on_comb(20480, 20480, 20480, 19968), 20480); } +// w=1.0,x=1.0,t=2.0,eta=0.5 -> e=-1.0,g=-1.0,delta=-0.5,w'=1.5 (20736). +test ascend { assert_eq(on_comb(20480, 20480, 20992, 19968), 20736); }