diff --git a/docs/NOW.md b/docs/NOW.md index b8a9abbca5..d9ef3c8350 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,7 +1,15 @@ -# NOW — ci: bit-exact emit gate makes the proof an invariant (2026-08-07) +# NOW — feat: parametric multi-output trainer, bit-exact (2026-08-07) Last updated: 2026-08-07 +## feat: lift n_out=1 -> fully parametric multi-output/multi-input, proven bit-exact (Refs #1764) + +- Removed the generator's last functional restriction. `emit_verilog` now emits a FULLY PARAMETRIC interface: one `x{k}i` port per input, one `t{o}i` port per output, and a packed `yout` ([32*n_out-1:0], y0 in the LSB word). Every target is driven -> no uninitialized-`t1` divergence (the bug the cross-check caught last cycle is now impossible) +- **Bit-exact gate extended to compare EVERY output per step** across 8 topologies incl. multi-output (2,2,2)/(2,4,2)/(2,3,3) and multi-input (3,4,2): **RTL == model BIT-EXACT over 80 training steps, all outputs** -- the previously-diverging (2,2,2) now passes +- Python self-test: added a (2,4,2) one-hot 2-class classifier that LEARNS (held-out 56/60, argmax over the 2 outputs) -- confirms the multi-output backprop algorithm is correct, not just self-consistent +- Debugging note baked into the gate: an inline sequence of many `wait(done)` in one `initial` block hangs under iverilog -> the harness drives via a per-arch `task` (proven handshake) +- => the programmable trainer now generates ANY 2-layer topology (inputs x hidden x outputs), each proven bit-exact spec->RTL. Tool+gate only; Refs #1764 + ## ci: emit_verilog bit-exactness is now a reproducible gate, not a one-off (Refs #1764) - Last cycle PROVED the generated trainer RTL bit-exact vs the model once, by hand. This cycle makes it an INVARIANT: `tools/verify_emit_bitexact.py` regenerates the GF-T cores FRESH from their .t27 specs (via t27c, per L2 GENERATION -- no hand-committed gen/), emits the microsequencer for hidden widths {2,3,4,5}, and cross-checks `yout` u32 per step in Icarus Verilog over an 80-step training run diff --git a/tools/gft_backprop_microcode.py b/tools/gft_backprop_microcode.py index f160110eaf..51558d1dcf 100644 --- a/tools/gft_backprop_microcode.py +++ b/tools/gft_backprop_microcode.py @@ -162,17 +162,17 @@ def run(steps, rf): def emit_verilog(n_in, n_hid, n_out, modname): """Emit a synthesizable microsequencer Verilog module for the given arch. One shared GftSmul + one shared GftSadd, a register file, and a case(pc) ROM. - Weights init small-random; build with `synth_xilinx -nocarry` (sequencer - counters hit the nextpnr CARRY4-placement bug). Bigger nets = same datapath, - ~constant area (measured: (2,2,1) 2.93M fasm, (2,3,1) 2.92M).""" + Fully parametric interface: one x{k}i input port per input, one t{o}i target + port per output, a packed yout ([32*n_out-1:0], y0 in the LSB word). Weights + init small-random; build with `synth_xilinx -nocarry` (sequencer counters hit + the nextpnr CARRY4-placement bug). Bigger nets = same datapath, ~constant area + (measured: (2,2,1) 2.93M fasm, (2,3,1) 2.92M).""" import random - # the emitted module hard-wires x0i/x1i/ti -> it can only carry 2 inputs and 1 - # target. Multi-output would need t1.. ports (else t1.. read as uninitialized x - # in RTL vs 0 in the model -> divergence). Hidden width is free; that is the - # "programmable size" axis the whitepaper claims. Guard the supported shape. - if n_in != 2 or n_out != 1: - raise ValueError(f"emit_verilog wires x0i/x1i/ti: supports n_in=2, n_out=1 " - f"(hidden width free); got n_in={n_in}, n_out={n_out}") + # Fully parametric interface: one x{k}i port per input, one t{o}i port per + # target, and a packed yout ([32*n_out-1:0], y0 in the LSB word). Every t{o} is + # driven, so no target register is read uninitialized (the old multi-output bug). + if n_in < 1 or n_hid < 1 or n_out < 1: + raise ValueError(f"emit_verilog needs n_in,n_hid,n_out >= 1; got {(n_in, n_hid, n_out)}") reg, steps = gen(n_in, n_hid, n_out); N = len(reg); NP = len(steps) random.seed(3); initv = {} for j in range(n_hid): @@ -182,8 +182,10 @@ def emit_verilog(n_in, n_hid, n_out, modname): for j in range(n_hid): initv[f"b{j}"] = round(random.uniform(-0.5, 0.5), 3) for o in range(n_out): initv[f"bo{o}"] = 0.0 pcw = max(1, NP.bit_length()); L = [] - L.append(f"module {modname}(input clk, input rst, input start, input [31:0] x0i," - f" input [31:0] x1i, input [31:0] ti, output reg [31:0] yout, output reg done);") + xports = ", ".join(f"input [31:0] x{k}i" for k in range(n_in)) + tports = ", ".join(f"input [31:0] t{o}i" for o in range(n_out)) + L.append(f"module {modname}(input clk, input rst, input start, {xports}, {tports}," + f" output reg [{32*n_out-1}:0] yout, output reg done);") L.append(f" reg [31:0] rf [0:{N-1}];") L.append(" function [31:0] modf(input [31:0] v, input [2:0] m); reg neg0; reg [6:0] off;" " reg [8:0] mant; begin neg0=v[16]; case(m)") @@ -206,10 +208,12 @@ def emit_verilog(n_in, n_hid, n_out, modname): L.append(f" for(gi=0;gi<{N};gi=gi+1) rf[gi]<=32'd0;") # zero scratch (match model's 0-init; no x-propagation) for name, val in initv.items(): L.append(f" rf[{reg[name]}]<=32'd{enc(val)};") L.append(" end else begin done<=0;") - L.append(f" if(!running) begin if(start) begin rf[{reg['x0']}]<=x0i; rf[{reg['x1']}]<=x1i;" - f" rf[{reg['t0']}]<=ti; pc<=0; settle<=SETTLE; running<=1; end end") + loads = " ".join(f"rf[{reg[f'x{k}']}]<=x{k}i;" for k in range(n_in)) \ + + " " + " ".join(f"rf[{reg[f't{o}']}]<=t{o}i;" for o in range(n_out)) + L.append(f" if(!running) begin if(start) begin {loads} pc<=0; settle<=SETTLE; running<=1; end end") + ypack = "{" + ", ".join(f"rf[{reg[f'y{o}']}]" for o in range(n_out - 1, -1, -1)) + "}" L.append(" else begin if(settle==0) begin rf[di] <= (op==2)? a_val : (op? add_r : mul_r);") - L.append(f" if(pc=={pcw}'d{NP-1}) begin running<=0; done<=1; yout<=rf[{reg['y0']}]; end" + L.append(f" if(pc=={pcw}'d{NP-1}) begin running<=0; done<=1; yout<={ypack}; end" " else begin pc<=pc+1'b1; settle<=SETTLE; end") L.append(" end else settle<=settle-1; end end end") L.append("endmodule") @@ -267,10 +271,41 @@ def _pred(a, b): assert "module bpseq231" in v and v.count("\n") > 40 assert "for(gi=0;gi<" in v, "scratch registers must be zero-inited on reset" print("emit_verilog: (2,3,1) module generated -- OK (build with -nocarry, ~2.9M fasm)") - # guard: the x0i/x1i/ti port shape only supports n_in=2, n_out=1 (hidden free) - for bad in [(2, 3, 2), (3, 3, 1)]: - try: - emit_verilog(*bad, "nope"); raise AssertionError(f"emit_verilog{bad} should have raised") - except ValueError: - pass - print("emit_verilog: rejects unsupported port shapes (n_in!=2 or n_out!=1) -- OK") + # multi-output: (2,4,2) module emits one x/t port per input/output + packed yout + v2 = emit_verilog(2, 4, 2, "bpseq242") + assert "input [31:0] x0i, input [31:0] x1i" in v2 + assert "input [31:0] t0i, input [31:0] t1i" in v2 + assert "output reg [63:0] yout" in v2, "n_out=2 packs two 32-bit outputs" + print("emit_verilog: (2,4,2) multi-output module generated -- OK (2 x/t ports, packed yout)") + # multi-output LEARNING: (2,4,2) one-hot 2-class quadrant task, argmax over outputs + reg, steps = gen(2, 4, 2); rf = [0] * len(reg) + random.seed(5) + for j in range(4): + for k in range(2): rf[reg[f"W{j}_{k}"]] = enc(round(random.uniform(-1, 1), 3)) + rf[reg[f"b{j}"]] = enc(round(random.uniform(-0.5, 0.5), 3)) + for o in range(2): + for j in range(4): rf[reg[f"v{o}_{j}"]] = enc(round(random.uniform(-1, 1), 3)) + random.seed(9) + def _cls(a, b): return int((a > 0) != (b > 0)) + def _ds2(n): + d = [] + while len(d) < n: + a = random.uniform(-1, 1); b = random.uniform(-1, 1) + if abs(a) < 0.15 or abs(b) < 0.15: continue + d.append((a, b, _cls(a, b))) + return d + tr2, te2 = _ds2(160), _ds2(60) + def _pred2(a, b): + sav = rf[:]; rf[reg["x0"]] = enc(a); rf[reg["x1"]] = enc(b) + rf[reg["t0"]] = 0; rf[reg["t1"]] = 0; run(steps, rf) + ys = [dec(rf[reg[f"y{o}"]]) for o in range(2)] + for i in range(len(rf)): rf[i] = sav[i] + return 0 if ys[0] >= ys[1] else 1 + for _ in range(60): + for a, b, c in tr2: + rf[reg["x0"]] = enc(a); rf[reg["x1"]] = enc(b) + rf[reg["t0"]] = enc(1.0 if c == 0 else 0.0); rf[reg["t1"]] = enc(1.0 if c == 1 else 0.0) + run(steps, rf) + te = sum(1 for a, b, c in te2 if _pred2(a, b) == c) + assert te >= int(0.9 * len(te2)), f"multi-output held-out too low: {te}/{len(te2)}" + print(f"self-test: (2,4,2) multi-output one-hot classifier, held-out {te}/{len(te2)} (>=90%) -- OK") diff --git a/tools/verify_emit_bitexact.py b/tools/verify_emit_bitexact.py index 10d0f79887..9a5c9da896 100644 --- a/tools/verify_emit_bitexact.py +++ b/tools/verify_emit_bitexact.py @@ -2,9 +2,10 @@ """Bit-exact gate for the programmable trainer's generated RTL. Regenerates the GF-T arithmetic cores from their .t27 specs (via t27c), emits the -microsequencer for several hidden widths via emit_verilog(), and proves in a -simulator that the generated RTL is BIT-EXACT to the Python GF-T model over a full -training run (forward + backprop + weight update), comparing yout u32 per step. +microsequencer for several topologies (varying hidden width, output count, and +input count) via emit_verilog(), and proves in a simulator that the generated RTL +is BIT-EXACT to the Python GF-T model over a full training run (forward + backprop ++ weight update), comparing EVERY output's u32 per step. Self-contained and CI-friendly: if t27c or iverilog is unavailable it prints SKIP and exits 0 (so it never breaks a Rust-only CI); a real mismatch exits 1. Run: @@ -15,7 +16,8 @@ ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) SMUL_SPEC = os.path.join(ROOT, "specs/ternary/gft_smul.t27") SADD_SPEC = os.path.join(ROOT, "specs/ternary/gft_sadd.t27") -ARCHS = [(2, 2, 1), (2, 3, 1), (2, 4, 1), (2, 5, 1)] # hidden width is the free axis +ARCHS = [(2, 2, 1), (2, 3, 1), (2, 4, 1), (2, 5, 1), # hidden-width axis + (2, 2, 2), (2, 4, 2), (2, 3, 3), (3, 4, 2)] # multi-output + multi-input STEPS = 80 @@ -47,33 +49,56 @@ def gen_core(t27c, spec, out): def check(g, arch, workdir): + n_in, n_hid, n_out = arch v = g.emit_verilog(*arch, "bpx") reg, steps = g.gen(*arch) rf = [0] * len(reg) for idx, val in re.findall(r"rf\[(\d+)\]<=32'd(\d+);", v): rf[int(idx)] = int(val) + # deterministic stream: n_in inputs + n_out targets per step (values arbitrary; + # bit-exactness is independent of target semantics, we just need identical drive) random.seed(101) seq = [] for _ in range(STEPS): - a = round(random.uniform(-1, 1), 3); b = round(random.uniform(-1, 1), 3) - t = float(int((a > 0) != (b > 0))) - seq.append((a, b, t)) + xs = [round(random.uniform(-1, 1), 3) for _ in range(n_in)] + cls = int((xs[0] > 0) != (xs[-1] > 0)) + ts = [1.0 if o == cls % n_out else 0.0 for o in range(n_out)] + seq.append((xs, ts)) py = [] - for (a, b, t) in seq: - rf[reg["x0"]] = g.enc(a); rf[reg["x1"]] = g.enc(b); rf[reg["t0"]] = g.enc(t) - g.run(steps, rf); py.append(rf[reg["y0"]] & 0xFFFFFFFF) + for (xs, ts) in seq: + for k in range(n_in): rf[reg[f"x{k}"]] = g.enc(xs[k]) + for o in range(n_out): rf[reg[f"t{o}"]] = g.enc(ts[o]) + g.run(steps, rf) + py.append(tuple(rf[reg[f"y{o}"]] & 0xFFFFFFFF for o in range(n_out))) + xdecl = " ".join(f"reg [31:0] x{k}=0;" for k in range(n_in)) + tdecl = " ".join(f"reg [31:0] t{o}=0;" for o in range(n_out)) + ports = ",".join([".clk(clk)", ".rst(rst)", ".start(start)"] + + [f".x{k}i(x{k})" for k in range(n_in)] + + [f".t{o}i(t{o})" for o in range(n_out)] + + [".yout(y)", ".done(done)"]) + # a per-arch task carries the proven start/wait(done) handshake (an inline + # sequence of many wait(done)'s in one initial block hangs under iverilog) + tparams = ", ".join([f"input [31:0] px{k}" for k in range(n_in)] + + [f"input [31:0] pt{o}" for o in range(n_out)]) + tassign = " ".join(f"x{k}=px{k};" for k in range(n_in)) \ + + " " + " ".join(f"t{o}=pt{o};" for o in range(n_out)) + fmt = "Y" + " %0d" * n_out + args = ",".join(f"y[{32*o} +: 32]" for o in range(n_out)) tb = [v, "`timescale 1ns/1ps", "module tb;", " reg clk=0; always #2.5 clk=~clk;", - " reg rst=1,start=0; reg [31:0] x0=0,x1=0,t=0; wire [31:0] y; wire done;", - " bpx dut(.clk(clk),.rst(rst),.start(start),.x0i(x0),.x1i(x1),.ti(t),.yout(y),.done(done));", - " task step(input [31:0] a,input [31:0] b,input [31:0] tt); begin", - " x0=a;x1=b;t=tt;@(posedge clk);start=1;@(posedge clk);start=0;wait(done);@(posedge clk);$display(\"Y %0d\",y);", + f" reg rst=1,start=0; {xdecl} {tdecl} wire [{32*n_out-1}:0] y; wire done;", + f" bpx dut({ports});", + f" task step({tparams}); begin", + f" {tassign} @(posedge clk); start=1; @(posedge clk); start=0;" + f" wait(done); @(posedge clk); $display(\"{fmt}\",{args});", " end endtask", " initial begin rst=1; repeat(6)@(posedge clk); rst=0; @(posedge clk);"] - for (a, b, t) in seq: - tb.append(f" step(32'd{g.enc(a)},32'd{g.enc(b)},32'd{g.enc(t)});") + for (xs, ts) in seq: + vals = ",".join([f"32'd{g.enc(xs[k])}" for k in range(n_in)] + + [f"32'd{g.enc(ts[o])}" for o in range(n_out)]) + tb.append(f" step({vals});") tb += [" $display(\"END\"); $finish; end", - " initial begin #40000000 $display(\"TIMEOUT\"); $finish; end", "endmodule"] + " initial begin #60000000 $display(\"TIMEOUT\"); $finish; end", "endmodule"] tbf = os.path.join(workdir, "tb.v"); open(tbf, "w").write("\n".join(tb)) vvp = os.path.join(workdir, "tb.vvp") r = subprocess.run(["iverilog", "-o", vvp, tbf, @@ -82,14 +107,14 @@ def check(g, arch, workdir): if r.returncode != 0: print(f"FAIL {arch}: iverilog compile error\n{r.stderr}"); return False out = subprocess.run(["vvp", vvp], capture_output=True, text=True).stdout - rtl = [int(x) for x in re.findall(r"^Y (\d+)$", out, re.M)] + rtl = [tuple(map(int, m.split())) for m in re.findall(r"^Y ([\d ]+)$", out, re.M)] if len(rtl) != len(py): print(f"FAIL {arch}: step count RTL={len(rtl)} PY={len(py)}"); return False mism = [(i, p, r_) for i, (p, r_) in enumerate(zip(py, rtl)) if p != r_] if mism: print(f"FAIL {arch}: {len(mism)}/{len(py)}; first step {mism[0][0]} py={mism[0][1]} rtl={mism[0][2]}") return False - print(f"OK {arch}: RTL == model BIT-EXACT over {len(py)} training steps (final yout={py[-1]})") + print(f"OK {arch}: RTL == model BIT-EXACT over {len(py)} training steps, all {n_out} output(s) (final yout={py[-1]})") return True