diff --git a/docs/NOW.md b/docs/NOW.md index 160e060412..c0ba0c5478 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,7 +1,15 @@ -# NOW — ci: emit gate now also proves SYNTHESIZABILITY (2026-08-07) +# NOW — feat: arbitrary-DEPTH trainer (>2 layers), proven bit-exact + synth (2026-08-07) Last updated: 2026-08-07 +## feat: lift the 2-layer restriction -> arbitrary-depth net, bit-exact + synthesizable (Refs #1764) + +- Removed the generator's last STRUCTURAL restriction (exactly 2 layers). New `gen_deep(sizes)` + `emit_verilog_deep(sizes)` produce full backprop for an L-layer net of ANY depth (`sizes=[n_in,h1,...,n_out]`): hidden layers ReLU, linear output, deltas propagated back-to-front through every hidden layer. Naming stays emit-compatible (x{k}/t{o}/y{o}) +- Refactored the shared Verilog emitter into `_emit_module` so the 2-layer (`emit_verilog`) and deep (`emit_verilog_deep`) paths do not duplicate; `emit_verilog` output unchanged; `gen_deep([n_in,n_hid,n_out])` matches `gen()` step-for-step (26 regs/47 steps for [2,3,1]) +- **Same tiny datapath (one smul + one sadd): depth costs microcode STEPS (time), not FPGA area** -- [2,4,3,1] synthesizes to 17672 cells, comparable to the 2-layer (2,4,2)'s 17468 +- Proven: self-test [2,4,3,1] (3-layer, 2 hidden) LEARNS the noisy nonlinear task (held-out 59/60); bit-exact gate extended with deep archs [2,4,3,1], [2,5,3,2] (deep+multi-out), [3,4,4,2,1] (**4-layer, 3 hidden**) -- all RTL == model bit-exact over 80 steps, and [2,4,3,1] added to the synth gate +- => the generator now emits ANY feed-forward topology (arbitrary inputs x hidden-layers x outputs), each proven bit-exact spec->RTL AND synthesizable in CI. No structural restrictions remain. Tool+gate only; Refs #1764 + ## ci: emit-bitexact gate adds a yosys synth_xilinx check (Refs #1764) - The gate proved semantic equivalence (iverilog bit-exact) but not that the emitted RTL SYNTHESIZES -- a change can stay bit-exact in sim yet break synthesizability (non-synth construct) and only fail when a bitstream is attempted on silicon diff --git a/tools/gft_backprop_microcode.py b/tools/gft_backprop_microcode.py index 51558d1dcf..905ca61f25 100644 --- a/tools/gft_backprop_microcode.py +++ b/tools/gft_backprop_microcode.py @@ -76,6 +76,71 @@ def ADD(a, am, b, bm, d): S.append(("ADD", reg[a], am, reg[b], bm, reg[d])) ADD(f"b{j}", 0, f"dz{j}", 4, f"b{j}") return reg, S + +def gen_deep(sizes): + """Return (reg_map, steps) for the full backprop of an L-layer net of arbitrary + DEPTH. `sizes` = [n_in, h1, h2, ..., n_out] (>=2 entries => >=1 weight layer). + Hidden layers use ReLU; the output layer is linear (logits). Naming stays + emit-compatible: inputs x{k}, targets t{o}, outputs y{o}. A 2-layer net + [n_in, n_hid, n_out] is functionally identical to gen(n_in, n_hid, n_out).""" + assert len(sizes) >= 2, "need at least [n_in, n_out]" + L = len(sizes) - 1 # number of weight layers + idx = [0]; reg = {} + def alloc(name): reg[name] = idx[0]; idx[0] += 1; return reg[name] + # weights W{l}_{j}_{k}: layer l unit j <- layer l-1 unit k ; biases b{l}_{j} + for l in range(1, L + 1): + for j in range(sizes[l]): + for k in range(sizes[l - 1]): alloc(f"W{l}_{j}_{k}") + for l in range(1, L + 1): + for j in range(sizes[l]): alloc(f"b{l}_{j}") + for k in range(sizes[0]): alloc(f"x{k}") + for o in range(sizes[L]): alloc(f"t{o}") + for l in range(1, L): # hidden pre-activations z{l}_{j} + for j in range(sizes[l]): alloc(f"z{l}_{j}") + for o in range(sizes[L]): alloc(f"y{o}") # linear outputs (== z^L) + for o in range(sizes[L]): alloc(f"e{o}") # output error = y - t = delta^L + for l in range(1, L): # hidden deltas d{l}_{j} + for j in range(sizes[l]): alloc(f"d{l}_{j}") + alloc("m1"); alloc("acc") + S = [] + def MUL(a, am, b, bm, d): S.append(("MUL", reg[a], am, reg[b], bm, reg[d])) + def ADD(a, am, b, bm, d): S.append(("ADD", reg[a], am, reg[b], bm, reg[d])) + def act(l, k): # activation reg + read-mod of layer l unit k + return (f"x{k}", 0) if l == 0 else (f"z{l}_{k}", 1) # input raw / hidden relu + def dst_pre(l, j): # where layer l's pre-activation is stored + return f"y{j}" if l == L else f"z{l}_{j}" + def delta(l, u): # delta reg of layer l unit u + return f"e{u}" if l == L else f"d{l}_{u}" + # forward: z^l_j = W^l_j . a^{l-1} + b^l_j + for l in range(1, L + 1): + for j in range(sizes[l]): + r0, m0 = act(l - 1, 0) + MUL(f"W{l}_{j}_0", 0, r0, m0, "acc") + for k in range(1, sizes[l - 1]): + rk, mk = act(l - 1, k) + MUL(f"W{l}_{j}_{k}", 0, rk, mk, "m1"); ADD("acc", 0, "m1", 0, "acc") + ADD("acc", 0, f"b{l}_{j}", 0, dst_pre(l, j)) + # output error: e_o = y_o - t_o (delta^L, linear output) + for o in range(sizes[L]): + ADD(f"y{o}", 0, f"t{o}", 3, f"e{o}") + # hidden deltas (back-to-front): d^l_j = relu'(z^l_j) * sum_u W^{l+1}_{u,j} * delta^{l+1}_u + for l in range(L - 1, 0, -1): + for j in range(sizes[l]): + MUL(f"W{l+1}_0_{j}", 0, delta(l + 1, 0), 0, "acc") + for u in range(1, sizes[l + 1]): + MUL(f"W{l+1}_{u}_{j}", 0, delta(l + 1, u), 0, "m1"); ADD("acc", 0, "m1", 0, "acc") + MUL("acc", 0, f"z{l}_{j}", 2, f"d{l}_{j}") + # updates: W^l_{j,k} -= eta*delta^l_j*a^{l-1}_k ; b^l_j -= eta*delta^l_j + for l in range(1, L + 1): + for j in range(sizes[l]): + dj = delta(l, j) + for k in range(sizes[l - 1]): + rk, mk = act(l - 1, k) + MUL(dj, 0, rk, mk, "m1"); ADD(f"W{l}_{j}_{k}", 0, "m1", 4, f"W{l}_{j}_{k}") + ADD(f"b{l}_{j}", 0, dj, 4, f"b{l}_{j}") + return reg, S + + # ---- bit-faithful GF-T interpreter (self-test) ---- def _magmul(a16, b16): ao = a16 >> 9; am = a16 & 511; bo = b16 >> 9; bm = b16 & 511 @@ -181,6 +246,33 @@ def emit_verilog(n_in, n_hid, n_out, modname): for j in range(n_hid): initv[f"v{o}_{j}"] = round(random.uniform(-1.0, 1.0), 3) 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 + return _emit_module(reg, steps, initv, n_in, n_out, modname) + + +def emit_verilog_deep(sizes, modname): + """Emit the microsequencer for an arbitrary-DEPTH net (see gen_deep). `sizes` = + [n_in, h1, ..., n_out]. Same one-smul/one-sadd datapath and parametric interface + as emit_verilog; depth costs microcode steps (time), not area. A 2-entry-hidden + 2-layer `sizes` is equivalent to emit_verilog(n_in, n_hid, n_out).""" + import random + if len(sizes) < 2 or any(s < 1 for s in sizes): + raise ValueError(f"emit_verilog_deep needs sizes=[n_in,...,n_out] all >=1; got {sizes}") + L = len(sizes) - 1 + reg, steps = gen_deep(sizes) + random.seed(3); initv = {} + for l in range(1, L + 1): + for j in range(sizes[l]): + for k in range(sizes[l - 1]): initv[f"W{l}_{j}_{k}"] = round(random.uniform(-0.8, 0.8), 3) + for l in range(1, L + 1): + for j in range(sizes[l]): initv[f"b{l}_{j}"] = round(random.uniform(-0.5, 0.5), 3) + return _emit_module(reg, steps, initv, sizes[0], sizes[-1], modname) + + +def _emit_module(reg, steps, initv, n_in, n_out, modname): + """Shared Verilog emitter: one GftSmul + one GftSadd + register file + case(pc) + microcode ROM. Parametric ports (x{k}i / t{o}i / packed yout). Zero-inits the + whole rf on reset (RTL == model, no x-propagation).""" + N = len(reg); NP = len(steps) pcw = max(1, NP.bit_length()); L = [] 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)) @@ -309,3 +401,27 @@ def _pred2(a, b): 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") + # DEEP: a 3-layer [2,4,3,1] net (arbitrary depth, backprop through 2 hidden + # layers) learns the same noisy nonlinear task -- depth costs time, not area + reg, steps = gen_deep([2, 4, 3, 1]); rf = [0] * len(reg) + random.seed(3) + for l in range(1, 4): + for j in range([2, 4, 3, 1][l]): + for k in range([2, 4, 3, 1][l - 1]): rf[reg[f"W{l}_{j}_{k}"]] = enc(round(random.uniform(-0.8, 0.8), 3)) + rf[reg[f"b{l}_{j}"]] = enc(round(random.uniform(-0.5, 0.5), 3)) + random.seed(7) + trd, ted = _ds(160), _ds(60) + def _predd(a, b): + sav = rf[:]; rf[reg["x0"]] = enc(a); rf[reg["x1"]] = enc(b); rf[reg["t0"]] = 0 + run(steps, rf); y = dec(rf[reg["y0"]]) + for i in range(len(rf)): rf[i] = sav[i] + return int(y > 0.5) + for _ in range(60): + for a, b, t in trd: + rf[reg["x0"]] = enc(a); rf[reg["x1"]] = enc(b); rf[reg["t0"]] = enc(float(t)); run(steps, rf) + te = sum(1 for a, b, t in ted if _predd(a, b) == t) + assert te >= int(0.9 * len(ted)), f"deep [2,4,3,1] held-out too low: {te}/{len(ted)}" + print(f"self-test: deep [2,4,3,1] (3-layer, 2 hidden) learns nonlinear task, held-out {te}/{len(ted)} (>=90%) -- OK") + vd = emit_verilog_deep([2, 4, 3, 1], "deep431") + assert "module deep431" in vd and "for(gi=0;gi<" in vd + print("emit_verilog_deep: [2,4,3,1] module generated -- OK") diff --git a/tools/verify_emit_bitexact.py b/tools/verify_emit_bitexact.py index a0195ecda6..aa62a6848b 100644 --- a/tools/verify_emit_bitexact.py +++ b/tools/verify_emit_bitexact.py @@ -2,10 +2,11 @@ """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 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. +microsequencer for several topologies (varying hidden width, output count, input +count, and DEPTH -- 2- to 4-layer nets via emit_verilog / emit_verilog_deep), 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. Then, if yosys is present, it SYNTHESIZES the emitted RTL (synth_xilinx) for a couple of topologies and asserts a non-zero FF+LUT mapping -- catching a change @@ -22,8 +23,9 @@ 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 axis - (2, 2, 2), (2, 4, 2), (2, 3, 3), (3, 4, 2)] # multi-output + multi-input -SYNTH_ARCHS = [(2, 2, 1), (2, 4, 2)] # one single-output + one multi-output (yosys is slower) + (2, 2, 2), (2, 4, 2), (2, 3, 3), (3, 4, 2), # multi-output + multi-input + [2, 4, 3, 1], [2, 5, 3, 2], [3, 4, 4, 2, 1]] # DEEP (lists): 3- and 4-layer +SYNTH_ARCHS = [(2, 2, 1), (2, 4, 2), [2, 4, 3, 1]] # single / multi-out / deep (yosys is slower) STEPS = 80 @@ -54,10 +56,17 @@ def gen_core(t27c, spec, out): open(out, "w").write(v.stdout) +def _emit_and_gen(g, arch, modname="bpx"): + """Resolve arch -> (verilog, reg, steps, n_in, n_out). A 3-tuple is the 2-layer + path (gen/emit_verilog); a list [n_in,...,n_out] is the deep path.""" + if isinstance(arch, list): + return g.emit_verilog_deep(arch, modname), *g.gen_deep(arch), arch[0], arch[-1] + v = g.emit_verilog(*arch, modname); reg, steps = g.gen(*arch) + return v, reg, steps, arch[0], arch[2] + + def check(g, arch, workdir): - n_in, n_hid, n_out = arch - v = g.emit_verilog(*arch, "bpx") - reg, steps = g.gen(*arch) + v, reg, steps, n_in, n_out = _emit_and_gen(g, arch) rf = [0] * len(reg) for idx, val in re.findall(r"rf\[(\d+)\]<=32'd(\d+);", v): rf[int(idx)] = int(val) @@ -131,7 +140,7 @@ def synth_check(g, arch, workdir): empty module but map to ~0 cells). Uses the version-stable `Number of cells` stat line rather than parsing per-primitive names (which vary across yosys versions); reports the FF/LUT breakdown when it is parseable.""" - open(os.path.join(workdir, "bpx.v"), "w").write(g.emit_verilog(*arch, "bpx")) + open(os.path.join(workdir, "bpx.v"), "w").write(_emit_and_gen(g, arch)[0]) # -DSIMULATION strips the cores' `ifndef SIMULATION` self-test blocks. cmd = ("read_verilog -DSIMULATION bpx.v GftSmul.v GftSadd.v; hierarchy -top bpx; " "synth_xilinx -nocarry -flatten; stat")