diff --git a/docs/NOW.md b/docs/NOW.md index af6e403b21..df0661fb46 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,7 +1,13 @@ -# NOW — test: cross-target verification hardened to EXTREME operands (2026-08-07) +# NOW — test: cross-target coverage adds the sadd cancellation edge (2026-08-07) Last updated: 2026-08-07 +## 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) diff --git a/tools/verify_multitarget.py b/tools/verify_multitarget.py index f654b665eb..3f325ffa42 100644 --- a/tools/verify_multitarget.py +++ b/tools/verify_multitarget.py @@ -52,7 +52,16 @@ def gen_pairs(g): 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)] + 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 def py_ref(g, fn, pairs):