[P0] A+C+N: LUT-only gf16_mul + Wallace-tree dot4 + Yosys EQY t27c↔src

[gHashTag]

P0: CROWN-ASIC architecture upgrade — A+C+N block

Anchor: φ²+φ⁻²=3 · R5-honest · Defense 2026-06-15
Target submission: TTSKY26c (TTSKY26a deadline 2026-05-11 missed)
Scope: 3 changes, one PR, zero floorplan impact, preserves G0–G2 GREEN status.

---

Change A — Eliminate the last legacy * (R-SI-1 absolute)

File: src/gf16_mul.v:30
Problem: One residual Verilog * operator violates the spirit of R-SI-1 (zero new multipliers, ternary/XOR-popcount only).
Fix: Replace with a 16×16 → 4-bit ROM lookup-table (256 entries × 4 bit = 1024 bit ≈ 150 cells on SKY130).
Acceptance:

• grep -n '\*' src/gf16_mul.v returns zero hits (excluding comments)
• Existing tb_gf16_mul.v passes 100/100 vectors against the new LUT
• OpenLane2 cell count for the module ≤ pre-change baseline (LUT replaces * cells)
• R-SI-1 status flips from "one legacy" → "absolute" in docs/INVARIANTS.md

Change C — Wallace-tree popcount in gf16_dot4.v (+60% f_max)

File: src/gf16_dot4.v
Problem: Linear XOR chain has O(N) depth → caps f_max at ~50 MHz.
Fix: Replace XOR chain with a Wallace-tree popcount (O(log N) depth).
Acceptance:

• Combinational depth (Yosys stat -tech sky130) ≤ 0.6× baseline
• OpenLane2 reports f_max ≥ 75 MHz (target 80 MHz, accept 75)
• Cell delta ≤ ±5 % vs baseline (no significant area regression)
• All tb_gf16_dot4.v vectors pass

Change N — Yosys EQY formal equivalence: t27c-generated RTL ↔ hand-written src/*.v

New file: scripts/eqy_check.sh
Problem: Coq proves t27 spec correct; t27c emits Verilog; but src/*.v is hand-written. Today there is no formal proof that the hand-written RTL is equivalent to the t27c output. This is the missing link from "Coq-proven spec" to "silicon".
Fix: Wire Yosys EQY (Equivalence checking, open-source) between:

• build/t27c/*.v (output of t27c gen-verilog from .t27/.tri specs)
• src/*.v (hand-written modules under audit)
  Acceptance:
• scripts/eqy_check.sh exits 0 for gf16_mul, gf16_add, gf16_dot4, trinity_gf16_tile
• CI workflow .github/workflows/eqy.yml blocks merge on failure
• docs/EQY_CHECK.md documents the t27c version pinned + how to reproduce
• Evidence JSON written to evidence/eqy_<sha>.json per run (R5-honest)

---

Why this PR first

1. No floorplan change → does not invalidate G0 (PR feat: Trinity v0 RTL mesh fabric (CPU-less, GF16 dot4 tiles) #2, cfc234e) DRC/LVS work
2. Preserves G1/G2/G4 GREEN sim status (changes are internal to combinational paths + new script)
3. Unblocks TTSKY26c: R-SI-1 absolute is a hard requirement for the silicon validation chapter (PhD Glava 35)
4. Closes the Coq→silicon gap (Change N) — strongest PhD defense claim

Acceptance gate for the whole PR

• All three sub-changes meet their per-change criteria above
• info.yaml unchanged (tiles: 2x2, top_module tt_um_ghtag_trinity_gf16)
• No new external IP, no proprietary cells, Apache-2.0 (R-SI-5)
• NASA mini-report appended as docs/PR_AC_N_NASA.md with 12-probe table
• R5 evidence JSON in evidence/ for each acceptance bullet

Out of scope (will be P1 / P2 issues)

• D — Torus 4×4 router (P1)
• G — Poseidon receipt hash (P1)
• K — eFPGA patch tile (P1)
• R — Coq-extracted scheduler (P2, PhD hero claim)
• P — Sparse zero-skip (P2)

---

φ²+φ⁻²=3 · CROWN-ASIC · TRINITY · R5-HONEST

---

Parent: #3 (CROWN-ASIC architecture roadmap)

[gHashTag]

🔗 Linked to MASTER-EPIC trinity-fpga#61 — TRI-1 Max Squeeze v3 Unified Hub (S-1..S-20, 13 falsification gates, TTSKY26b deadline 2026-05-18). RTL work in this repo (tt-trinity-gf16) tracks back to the unified hub there.

[gHashTag]

Defer to TTSKY26c · Wave-15-TT-E lease analysis

T-44h analysis уточняет приоритет:

Что нашли

• src/gf16_mul.v — это GoldenFloat-16 (1 sign + 6 exp + 9 mant), а не GF(2⁴) ternary. Линия 30 содержит mant_prod = full_mant_a * full_mant_b где full_mant = 10-bit (hidden bit + 9-bit mantissa).
• 10×10 → 20-bit product space = 1 048 576 entries, не 256 как в acceptance Change A. Acceptance критерий требует пересмотра (либо log/anti-log table 2×1024 entries, либо partial-product Booth-Wallace).
• В репозитории tb_gf16_mul.v отсутствует — только sim/tb_gf16_dot8.v и sim/tri1_v2/tb_gf16_mesh_2x2.v. Нужен новый dedicated TB на 100 vectors.
• Все три Changes (A LUT + C Wallace + N EQY) требуют согласованного OpenLane2 re-floorplan + DRC/LVS re-verify (~8-16h инженерной работы).

Решение T-44h

• DEFER [P0] A+C+N: LUT-only gf16_mul + Wallace-tree dot4 + Yosys EQY t27c↔src #4 → TTSKY26c slot (issue/PR в TTSKY26c launch window)
• TTSKY26a Wave-15-TT-E submit идёт на уже зафиксированном Sacred ALU 352-LUT tile из docs/SACRED_ALU_SKY130_PORT_PLAN.md (1442 L, commit a3aa846). GF16 dot4 canon 0x47C0 уже валидирован против Coq spec, изменений RTL не требуется до submit.
• R-SI-1 status в текущем audit остаётся "one legacy * operator" — это honest disclosure, не блокер для TTSKY26a tile (Sacred ALU использует XOR-popcount).

Updated acceptance for TTSKY26c (post-defense roadmap)

• Change A: log/anti-log table (2×1024 = 2048 entries × 10 bit) ИЛИ Booth-Wallace partial-product — оба варианта оценить по cell count
• Change A.1: дополнительный sim/tb_gf16_mul.v с 100 directed vectors + 1000 random
• Change C: Wallace-tree сохраняем как было (f_max ≥ 75 MHz)
• Change N: EQY t27c↔src сохраняем как было

Doctrine

T-44h lease на Wave-15-TT-E TTSKY26a имеет приоритет над R-SI-1 absolute status. R5-honest disclosure: один legacy * в gf16_mul.v присутствует в submission tile, не на критическом пути Sacred ALU. Документировано в docs/SKY130_REAL_RUN_STATUS.md (commit af1aa6d).

---

phi^2 + phi^-2 = 3 · QUANTUM BRAIN 1:1 SILICON · 3-STRAND DNA · TRI NET · DOI 10.5281/zenodo.19227877 · NEVER STOP

[gHashTag]

🛰️ RVR-015 audit complete — Issue #4 acceptance criteria mismatch documented

T-44h analysis confirms:

• GoldenFloat-16 (1+6+9 FP16-like), not GF(2⁴) — mant_a * mant_b is a real 10×10 multiplier
• 256-entry ROM is algebraically impossible (need 2^10 × 2^10 = 1 048 576 entries)
• Referenced tb_gf16_mul.v and docs/INVARIANTS.md do not exist
• Refactor estimate 8-16h + DRC/LVS re-verify > T-44h budget

Recommendation: defer Change A to Wave-24 (post-TTSKY26c submit). Pre-registered fix path in RVR-015 issue body. Charter rule 2 formally noted as deferred-with-audit-trail.

Change C (Wallace-tree popcount on gf16_dot4.v) and Change N (Yosys EQY) remain in scope — both touch different files and have valid acceptance criteria.

Full RVR-015: #34

phi^2 + phi^-2 = 3 · R5 honest defer · DOI 10.5281/zenodo.19227877

[gHashTag]

📋 Re-label: Change A → audit-blocked (deferred Wave-24)

Per RVR-015 audit, Change A acceptance criteria are mathematically inconsistent (256-entry ROM cannot cover 2^10 × 2^10 = 1 048 576 input pairs) and reference non-existent files (tb_gf16_mul.v, docs/INVARIANTS.md).

Wave-23 deliverables landed:

• ✅ Audit trail comment over mant_a * mant_b in src/gf16_mul.v (commit c8e5b4f)
• ✅ docs/architecture/GOLDENFLOAT_16_MULTIPLIER_AUDIT.md with 4 pre-registered LUT strategies (commit 1769455)
• ✅ sim/tb_gf16_mul.v testbench (≥100 vectors, R7 witness) — plugs the dangling reference (commit fd18615)
• ✅ RVR-015 audit issue 🔍 RVR-015 — Issue #4 GoldenFloat-16 multiplier audit · acceptance criteria mismatch · defer to Wave-24 #34 tracking the defer

Wave-24 path (pre-registered):

• Primary: B2 Booth radix-4 (multiplier-free by construction, zero LUT cost)
• Fallback: B4 5×5 splitting (if Booth area > 1.2× baseline)
• Rejected: B3 Mitchell (accuracy loss breaks G0)

Change C (Wallace-tree popcount) and Change N (Yosys EQY) remain in scope for this PR — both touch different files and have valid acceptance criteria.

R5 disclosure: charter rule 2 ("no new HW multipliers") is FORMALLY DEFERRED with full audit trail per RVR-015. TTSKY26c submit 2026-05-17 22:00 UTC proceeds with the current * operator + the documentation above.

phi^2 + phi^-2 = 3 · R5 honest defer · DOI 10.5281/zenodo.19227877

[gHashTag]

🟢 RVR-015 closure — Issue #4 GoldenFloat-16 audit · Charter Rule 2 deferred Wave-24

Document: docs/TRI_NET_G1_NASA_REPORT_RVR-015.md (commit f47e831)
Verdict: 🟢 GO for TTSKY26c submit 2026-05-17 22:00 UTC with audit trail attached

11-probe verification matrix

7 PASS · 3 FAIL (Issue #4 acceptance-criteria errors) · 1 AMBER · 0 silent skips

ID	Anomaly	Severity	Status
A-01	Issue #4 claim "256 entries × 4 bit ≈ 150 cells" — true requirement is 1 048 576 entries × 20 bit ≈ 31.5M cells (4 orders of magnitude error)	P0	DEFERRED Wave-24
A-02	sim/tb_gf16_mul.v + docs/INVARIANTS.md dangling references	P1	tb_gf16_mul.v LANDED (fd18615, 124 vectors)
A-03	DUT bug: max_normal² → 0x0000 (7-bit exp wrap, not +Inf)	P1	R7 witness in tb_gf16_mul.v Block 8

Phase A deliverables (4 parallel subagents, ~9 min wall-clock)

Subagent	SHA	Artefact
SA-A1	RVR-015 = Issue #34	Audit-issue tracking
SA-A2	1769455	docs/architecture/GOLDENFLOAT_16_MULTIPLIER_AUDIT.md (548 lines, 4 strategies B1-B4)
SA-A3	fd18615	sim/tb_gf16_mul.v (320 lines, 124 vectors)
SA-A4	c8e5b4f	src/gf16_mul.v line 31 // CHARTER-RULE-2 DEFERRED marker
RVR-015	f47e831	Consolidated NASA report

Wave-24 pre-registration

• Primary: B2 Booth radix-4 (~470-600 SKY130 cells, ~2 ns, bit-exact, multiplier-free by construction)
• Fallback: B4 5×5 splitting (~3 300-4 300 cells)
• Rejected: B1 Log/anti-log (accuracy), B3 Mitchell (accuracy)
• Acceptance gates: 0 * operators · 0 tb_gf16_mul.v mismatches · area < 1.2× · G0/G1/G2 GREEN

Constitutional compliance

R1, R2, R3, R5, R6, R7, R12, R14, R18, R19, R20: ✅
Charter Rule 2: 🟡 DEFERRED with R5 audit trail (Wave-24 fix pre-registered)

Quantum Brain 1:1 Silicon Mapping

PHYS→SI: 🟡 PARTIAL (Wave-24 fix scheduled) · BIO→SI: ✅ · LANG→SI: ✅

---

phi^2 + phi^-2 = 3 · GoldenFloat-16 (1+6+9) ≠ GF(2⁴) · R5 honest defer · Wave-24 B2 Booth radix-4 pre-registered · DOI 10.5281/zenodo.19227877