test: harden cross-target verification to extreme/saturation operands

docs/NOW.md

@@ -1,7 +1,13 @@
-# NOW — feat: extend IGLA RACE cross-target to systolic PE + 2 more gen findings (2026-08-07)
+# NOW — test: cross-target verification hardened to EXTREME operands (2026-08-07)
 
 Last updated: 2026-08-07
 
+## 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
+
 ## feat: IGLA RACE ternary_mac + systolic PE bit-exact across C/Rust/model (Refs #1764)
 
 - Extended the IGLA RACE bridge up the datapath: `verify_igla_race.py` now also cross-checks `systolic_ternary_pe` (the weight-stationary PE: `psum_out = psum_in + ternary_mul(a,w)`, i16 accumulator) across C + Rust + an independent reference over 800 vectors incl. edges (a=-128, invalid codes, i16 psum saturation): **C == Rust == reference BIT-EXACT**. Both ternary_mac and the systolic PE now multi-target-verified

tools/verify_multitarget.py

@@ -4,8 +4,11 @@
 `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 random operands -- closing the
-"one spec -> any target, bit-exact" claim across {Verilog, C, Rust, model}.
+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).
 
 Self-contained + CI-friendly: SKIPs (exit 0) if t27c / a C compiler / rustc is
 missing; a real cross-target divergence exits 1. Run:
@@ -40,8 +43,15 @@ def load_gen():
 
 def gen_pairs(g):
     random.seed(202)
-    vals = [g.enc(round(random.uniform(-4, 4), 3)) for _ in range(48)]
+    # moderate range (typical activations/weights)
+    vals = [g.enc(round(random.uniform(-4, 4), 3)) for _ in range(40)]
     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))
     return [(random.choice(vals), random.choice(vals)) for _ in range(N)]