fix(gen-verilog-sim): lower plain assert(cond, "msg") to an if-based check

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)
 

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.

bootstrap/stage0/FROZEN_HASH

@@ -1 +1 @@
-4c1aaad5309a81cc8685154eaf71a4abb76431b20ddc14e444e82686df5d1b5e
+f74459fc23c3c54e7a3c5c0e72b45b53f560bee4a0633b903d54ff7d0dc714e1

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.
 
 ---
 

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)
 

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):