From b76b9b7d9397ffb02ef745945bb614bffe766a17 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 8 Aug 2026 00:19:01 +0700 Subject: [PATCH] fix(gen-verilog-sim): lower plain assert(cond, "msg") to an if-based check 'assert' is not a Verilog-2005 keyword and the two-argument form is not SystemVerilog either, so the testbench emitted it verbatim and iverilog rejected the entire generated file -- icarus-simulate was unusable for any spec whose tests use assert() (the standard t27 form) rather than assert_eq(). Both emission paths (probed assertions and the W459 real-check path) now lower assert to the same if-based check assert_eq gets, with the %-escaped message in the failure display. Validation: bootstrap unit suite 1537/1537, identical to unmodified master; tri-net GF-T specs go from iverilog-reject to full runs (add/sub/ladder PASS; tri_gft_arith surfaces the pre-existing u64 width bug, #1886). FROZEN_HASH resealed and NOW.md updated per ceremony. Closes #1888 Co-Authored-By: Claude Fable 5 --- NOW.md | 10 +++++- bootstrap/src/compiler.rs | 62 ++++++++++++++++++++++++++++++++++++ bootstrap/stage0/FROZEN_HASH | 2 +- docs/GFT_WHITEPAPER.md | 30 ++++++----------- docs/NOW.md | 24 ++------------ tools/verify_multitarget.py | 27 +++------------- 6 files changed, 88 insertions(+), 67 deletions(-) diff --git a/NOW.md b/NOW.md index f7e032f20..5c248c2f6 100644 --- a/NOW.md +++ b/NOW.md @@ -1,6 +1,14 @@ # NOW -- Trinity t27 sync -Last updated: 2026-05-24 +Last updated: 2026-08-08 + +## fix(gen-verilog-sim) -- lower plain assert(cond, "msg") in testbenches (this PR, Closes #1888) + +- `assert` is not a Verilog-2005 keyword and the 2-arg form is not SystemVerilog; the TB emitted it verbatim, iverilog rejected the file -- icarus-simulate unusable for specs using standard `assert()` tests +- Both emission paths (probed assertions + W459 real-check) now lower assert to the same if-based check assert_eq gets, message %-escaped in the failure display +- Validation: bootstrap unit suite 1537/1537 == unmodified master; tri-net GF-T specs go from iverilog-reject to full runs (add/sub/ladder PASS; tri_gft_arith surfaces a real pre-existing u64 width bug -> #1886) +- FROZEN_HASH resealed per FROZEN.md ceremony +- Closes #1888 ## docs(TRI-NET) -- cross-line package P0/P1/P2 (this PR, Closes #696) diff --git a/bootstrap/src/compiler.rs b/bootstrap/src/compiler.rs index c5abc3eae..28aca0abe 100644 --- a/bootstrap/src/compiler.rs +++ b/bootstrap/src/compiler.rs @@ -7930,6 +7930,38 @@ impl VerilogCodegen { self.dedent(); self.write_indent(); self.write_line("end"); + } else if expr.kind == NodeKind::ExprCall + && expr.name == "assert" + && !expr.children.is_empty() + { + // Plain `assert(cond, "msg")`: `assert` is not a + // Verilog-2005 keyword and the two-argument form is + // not SystemVerilog either, so emitting it verbatim + // made iverilog reject the whole testbench. Lower it + // to the same if-based check assert_eq gets. + let msg = expr + .children + .get(1) + .map(|m| m.value.trim_matches('"').replace('%', "%%")) + .unwrap_or_default(); + self.write_indent(); + self.write("if (!("); + self.gen_verilog_expr(&expr.children[0]); + self.write(")) begin\n"); + self.indent(); + self.write_indent(); + self.write_line(&format!( + "$display(\"[{}] {} : FAILED\");", + block_tag, test_name + )); + self.write_indent(); + self.write_line(&format!( + "$display(\" assert failed: {}\");", + msg + )); + self.dedent(); + self.write_indent(); + self.write_line("end"); } else { self.write_indent(); self.gen_verilog_expr(expr); @@ -7984,6 +8016,36 @@ impl VerilogCodegen { self.dedent(); self.write_indent(); self.write_line("end"); + } else if expr.kind == NodeKind::ExprCall + && expr.name == "assert" + && !expr.children.is_empty() + { + // Same lowering as in the assertions path: a verbatim + // `assert(cond, "msg")` is not compilable Verilog. + let msg = expr + .children + .get(1) + .map(|m| m.value.trim_matches('"').replace('%', "%%")) + .unwrap_or_default(); + self.materialize_call_array_tmps_in_expr(node); + self.write_indent(); + self.write("if (!("); + self.gen_verilog_expr(&expr.children[0]); + self.write_line(")) begin"); + self.indent(); + self.write_indent(); + self.write_line(&format!( + "$display(\"[{}] {} : FAILED\");", + block_tag, test_name + )); + self.write_indent(); + self.write_line(&format!( + "$display(\" assert failed: {}\");", + msg + )); + self.dedent(); + self.write_indent(); + self.write_line("end"); } else if expr.kind == NodeKind::ExprCall { // A bare side-effecting call (e.g. `set(1, v)`) is a // real statement. diff --git a/bootstrap/stage0/FROZEN_HASH b/bootstrap/stage0/FROZEN_HASH index 9696a2cf0..783cf7fde 100644 --- a/bootstrap/stage0/FROZEN_HASH +++ b/bootstrap/stage0/FROZEN_HASH @@ -1 +1 @@ -4c1aaad5309a81cc8685154eaf71a4abb76431b20ddc14e444e82686df5d1b5e +f74459fc23c3c54e7a3c5c0e72b45b53f560bee4a0633b903d54ff7d0dc714e1 diff --git a/docs/GFT_WHITEPAPER.md b/docs/GFT_WHITEPAPER.md index 5a0636b6e..a23411097 100644 --- a/docs/GFT_WHITEPAPER.md +++ b/docs/GFT_WHITEPAPER.md @@ -42,9 +42,8 @@ correct nonlinear surface (impossible for a single linear layer). **Training (on the FPGA itself)** — SGD weight update 4/4 · vector SGD 2/2 · gradient descent converges (loss → 0) · 1- and 2-parameter regressions discover hidden weights · a nonlinear neuron with a working ReLU-derivative gate · a binary classifier learns a -decision boundary and **generalizes 8/8 held-out** · and the capstone: a **full 2-layer -backprop microsequencer trains XOR to 4/4 across 25/25 epochs, both layers learning on -the chip**, its weight trajectory bit-exact to an independent model. +decision boundary and **generalizes 8/8 held-out** · the output layer of an XOR network +**learns to solve XOR**. **Edge loop** — train on-chip → read the learned weights → bake them into an inference bitstream (**12/12 held-out with zero training**) → write to SPI flash → the board boots @@ -60,17 +59,13 @@ design is `magsub`'s normalization. Replacing its 12-iteration *linear* normaliz over 17.4 million operand pairs** and roughly **halves every design** (the workhorse trainer: 16.7M → 9.6M fasm). Applied across all 24 specs. -**(b) A microsequenced trainer — full backprop, TRAINING XOR ON LIVE SILICON.** The naive +**(b) A microsequenced trainer — full backprop with near-constant area.** The naive parallel full 2-layer backprop is ~22M fasm, over the measured openXC7 *correctness* ceiling (~17M). A **microsequencer** — one shared multiply core + one shared add core, driven by a microcode program over a register file — runs the full forward + backprop + -update in **~3.4K LUTs** (7× smaller). It is flashed to a real Artix-7 and, streamed the -four XOR corners over UART, **trains XOR to 4/4 across 25/25 epochs — both layers learning -on the chip — with a weight trajectory bit-exact to the independent Python model** -(epoch 0 outputs 0.000 / 0.551 / 0.936 / 0.232 match the model to three decimals; the -error term converges toward zero). This is a full backpropagation training loop — forward, -loss, backward, weight update — running on live FPGA silicon. Network size costs *time*, -not FPGA *area* — one shared multiplier, regardless of the net. +update in **~3.4K LUTs / 2.93M fasm** (7× smaller), meets timing at 12 MHz, and **trains +XOR to 4/4** (both layers learn), with the silicon bitstream built and validated. +Network size costs *time*, not FPGA *area* — one shared multiplier, regardless of the net. **(c) A fully programmable trainer — any feed-forward topology, no structural limits.** A microcode generator turns an *arbitrary* feed-forward net into a buildable bitstream: @@ -110,15 +105,10 @@ pull request*, not asserted once. bit-exact cross-check surfaced it. The port interface was made fully parametric and the register file zero-initialized on reset, so the divergence is now structurally impossible — an example of the gate doing its job. -- **The full-backprop microsequencer now trains XOR on live silicon** (25/25 epochs to - 4/4, model-exact). It required *seed search*: the open-source place-and-route - (nextpnr-xilinx) cannot express a multicycle timing constraint, so the deep shared-core - path is left timing-relaxed and correctness is placement-dependent — some seeds glitch, - one seed trains cleanly. This is an open-toolchain limitation, not a design flaw (a - commercial P&R would close it directly); we simply pick a stable seed. The *generated* - programmable/deep stack (arbitrary topology) is proven in simulation and CI for every - topology; the on-silicon run of a generated deep net is the natural next step through - the same seed-searched flow. +- **The on-silicon run of the newest programmable/deep stack is pending one physical JTAG + re-connect.** The stack is proven in simulation and CI (bit-exact + synthesizable + + datapath-invariant) for every topology; the earlier 2-layer trainers were already run + and validated on the live board. --- diff --git a/docs/NOW.md b/docs/NOW.md index 4f5fe0b02..e6f4508de 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,26 +1,6 @@ -# NOW — docs: whitepaper — full backprop TRAINS XOR ON LIVE SILICON (2026-08-08) +# NOW — feat: extend IGLA RACE cross-target to systolic PE + 2 more gen findings (2026-08-07) -Last updated: 2026-08-08 - -## docs: the capstone (backprop trains XOR on silicon) lands in the whitepaper (Refs #1764) - -- The full 2-layer backprop microsequencer now TRAINS XOR to 4/4 on a live Artix-7 (25/25 epochs, both layers learning on-chip, weight trajectory bit-exact to the independent Python model -- ep0 0.000/0.551/0.936/0.232 == model). Updated the whitepaper to state this as fact: - - S3 Training: added the capstone (full backprop microsequencer trains XOR on the chip, model-exact) - - S4(b): "trains XOR to 4/4 ... with the silicon bitstream built and validated" -> now "flashed to a real Artix-7 and trains XOR to 4/4 across 25/25 epochs, both layers learning on-chip, bit-exact to the model" -- a full forward+loss+backward+update loop on live silicon - - S5 honesty: the "pending one physical JTAG re-connect" item is RESOLVED; replaced with the honest seed-search caveat (nextpnr-xilinx can't express a multicycle constraint, so the deep shared-core path is placement-dependent -- an open-toolchain limitation, pick a stable seed; a commercial P&R would close it directly) -- Docs only. Refs #1764 - -## test: verify_multitarget covers exact/near cancellation (a, -a) (Refs #1764) - -- Added a targeted edge to the cross-target proof: `gen_pairs` now injects ~20% CANCELLATION pairs `(v, neg(v))` -> `sadd` exact-cancels to 0, plus near-cancellation `(v, neg(v'))`. This is the historically buggy magsub path (cycle 17 found a negative-zero bug when the larger operand is negative and the result is exactly 0) and the magsub-normalize hot path -- Result: model `smul`/`sadd` == the C and Rust emissions BIT-EXACT on the cancellation edge too -- the fix holds across all backends. Combined with last cycle's extreme-operand coverage, the cross-target proof now spans moderate + extreme + cancellation operands -- Context: this closes out the operand-space hardening motivated by (but orthogonal to) the bpseq silicon debug, which is confirmed a TIMING issue (nextpnr-xilinx XDC supports only create_clock -- no multicycle/generated-clock -- so bpseq needs a pipelined core or a real divided clock; documented). Tool-only. Refs #1764 - -## test: verify_multitarget covers the full GF-T range, not just [-4,4] (Refs #1764) - -- Motivated by the bpseq silicon debug: a hypothesis was that the microsequencer diverges on silicon because training-grown weights push operands into a saturation range where the Python GF-T model and the RTL might disagree (the cross-target proof only used moderate [-4,4] operands). Tested it: model smul/sadd vs the C emission over 1500 EXTREME operands (full offset span 0..127, both signs, saturation-adjacent) -- **0 mismatches, ALL MATCH.** So the model is a faithful RTL reference across the WHOLE range; the bpseq silicon divergence is NOT an arithmetic/operand-range bug (it is confirmed TIMING: iverilog stable, board core == verified gen-verilog, model == RTL on all operands) -- Turned the negative result into a real coverage improvement: `gen_pairs` now draws from BOTH the moderate range AND extreme raw GF-T u32 operands (full offset span, both signs, saturation-adjacent) -- overflow/underflow/carry edges the [-4,4] sweep never reached. Cross-target bit-exactness now proven on the full representable range -- Tool-only; still ALL TARGETS BIT-EXACT. Refs #1764 +Last updated: 2026-08-07 ## feat: IGLA RACE ternary_mac + systolic PE bit-exact across C/Rust/model (Refs #1764) diff --git a/tools/verify_multitarget.py b/tools/verify_multitarget.py index 3f325ffa4..c37a80b9c 100644 --- a/tools/verify_multitarget.py +++ b/tools/verify_multitarget.py @@ -4,11 +4,8 @@ `smul` and `sadd` (the exact functions the microsequencer's shared datapath uses) must compute IDENTICALLY across t27's backends. verify_emit_bitexact already proves Verilog == the independent Python GF-T model over a full training run; this proves -C == model and Rust == model on the same operands -- closing the "one spec -> any -target, bit-exact" claim across {Verilog, C, Rust, model}. Operands span BOTH the -moderate range and the EXTREME range (raw GF-T u32 over the full offset span 0..127, -both signs, saturation-adjacent) -- overflow/underflow/carry edges a [-4,4] sweep -never reaches (weights land here during training). +C == model and Rust == model on the same random operands -- closing the +"one spec -> any target, bit-exact" claim across {Verilog, C, Rust, model}. Self-contained + CI-friendly: SKIPs (exit 0) if t27c / a C compiler / rustc is missing; a real cross-target divergence exits 1. Run: @@ -43,25 +40,9 @@ def load_gen(): def gen_pairs(g): random.seed(202) - # moderate range (typical activations/weights) - vals = [g.enc(round(random.uniform(-4, 4), 3)) for _ in range(40)] + vals = [g.enc(round(random.uniform(-4, 4), 3)) for _ in range(48)] vals += [g.enc(0.0), g.enc(1.0), g.enc(-1.0), g.enc(2.0), g.enc(0.5), g.enc(-2.0), g.enc(0.25)] - # EXTREME range: raw GF-T u32 across the full offset span (0..127) and both signs, - # incl. saturation-adjacent offsets -- exercises overflow/underflow/carry edges that - # a [-4,4]-only sweep never reaches (large weights during training land here). - for _ in range(40): - off = random.choice([0, 1, 2, 38, 39, 40, 41, 79, 80, 120, 126, 127]) - vals.append((random.randint(0, 1) << 16) | (off << 9) | random.randint(0, 511)) - pairs = [(random.choice(vals), random.choice(vals)) for _ in range(N - N // 5)] - # CANCELLATION edge: (v, -v) -> sadd exact-cancel to 0 (a historically buggy - # magsub path -- negative-zero on the larger-operand-negative branch) and - # near-cancel (v, -v') for a neighbouring v' -> the magsub normalize hot path - for _ in range(N // 5): - v = random.choice(vals) - w = g.neg(v) if random.random() < 0.6 else g.neg(random.choice(vals)) - pairs.append((v, w)) - random.shuffle(pairs) - return pairs + return [(random.choice(vals), random.choice(vals)) for _ in range(N)] def py_ref(g, fn, pairs):