Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion docs/NOW.md
Original file line number Diff line number Diff line change
@@ -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
Expand Down
79 changes: 57 additions & 22 deletions tools/gft_backprop_microcode.py
Original file line number Diff line number Diff line change
Expand Up @@ -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):
Expand All @@ -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)")
Expand All @@ -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")
Expand Down Expand Up @@ -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")
63 changes: 44 additions & 19 deletions tools/verify_emit_bitexact.py
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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


Expand Down Expand Up @@ -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,
Expand All @@ -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


Expand Down
Loading