diff --git a/docs/NOW.md b/docs/NOW.md index e6f4508ded..af6e403b21 100644 --- a/docs/NOW.md +++ b/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 diff --git a/tools/verify_multitarget.py b/tools/verify_multitarget.py index c37a80b9cc..f654b665eb 100644 --- a/tools/verify_multitarget.py +++ b/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)]