[WAVE-24] feat(silicon): Yosys EQY t27c↔src formal equivalence gate · RVR-017 · DO NOT MERGE PRE-TTSKY26c

.github/workflows/eqy.yml

@@ -0,0 +1,188 @@
+name: eqy
+
+# =============================================================================
+# Yosys EQY formal equivalence gate — Wave-24 RVR-017 · Issue #4 Change N
+#
+# Purpose:
+#   Verify that hand-written src/*.v modules are formally equivalent to the
+#   reference Verilog generated by `t27c gen-verilog` from the t27 spec
+#   (repository gHashTag/t27 @ T27C_COMMIT).
+#
+# Verdicts:
+#   PASS    — EQY confirmed equivalence (blocks merge if any FAIL)
+#   FAIL    — EQY found non-equivalence  ← blocks merge
+#   PENDING — t27c reference file missing (warns, does NOT block)
+#
+# Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877
+# =============================================================================
+
+on:
+  push:
+    branches:
+      - '**'
+  pull_request:
+    branches:
+      - main
+      - 'feat/**'
+
+jobs:
+  eqy-check:
+    name: Yosys EQY t27c↔src equivalence
+    runs-on: ubuntu-22.04
+
+    env:
+      # Pinned gHashTag/t27 commit that owns the reference Verilog files.
+      # Update this when a new t27c gen-verilog run produces build/t27c/*.v
+      T27C_COMMIT: "9752bab4b81fe1a3abc66b13749c4ac412a74ee6"
+      # EQY_STRICT=0 — PENDING verdicts warn but do not fail CI
+      # Set to "1" after build/t27c/*.v are committed to block on PENDING
+      EQY_STRICT: "0"
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Install system dependencies
+        run: |
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends \
+            build-essential \
+            python3 \
+            python3-pip \
+            tcl \
+            libreadline-dev \
+            bison \
+            flex \
+            wget \
+            ca-certificates
+
+      - name: Install Yosys (pinned apt package)
+        run: |
+          # Install Yosys from apt — Ubuntu 22.04 ships Yosys 0.9 (uses -V not --version)
+          sudo apt-get install -y --no-install-recommends yosys
+          # Yosys 0.9 uses -V flag; newer versions support --version
+          yosys -V 2>/dev/null || yosys --version 2>/dev/null || echo "yosys installed (version flag varies)"
+
+      - name: Install Yosys EQY
+        # Non-fatal: if eqy is unavailable, script marks modules PENDING (R5-honest)
+        # EQY_STRICT=0 means PENDING verdicts warn but do not block CI
+        continue-on-error: true
+        run: |
+          # Install eqy from YosysHQ/eqy source (pip package name varies by version)
+          # Try multiple install methods in order; non-fatal per continue-on-error
+          pip3 install --user yosys-eqy 2>&1 && echo "Installed via pip yosys-eqy" && exit 0
+          echo "pip yosys-eqy failed, trying pip eqy..."
+          pip3 install --user eqy 2>&1 && echo "Installed via pip eqy" && exit 0
+          echo "Both pip methods failed. EQY will be marked NOT_INSTALLED."
+          echo "Modules will receive PENDING verdict (acceptable with EQY_STRICT=0)."
+          exit 0  # always succeed — script handles missing eqy gracefully
+
+      - name: Show toolchain versions
+        run: |
+          echo "=== Yosys version ==="
+          yosys -V 2>/dev/null || yosys --version 2>/dev/null || echo "yosys not found"
+          echo "=== EQY version ==="
+          eqy --version 2>/dev/null || echo "eqy not found (will mark PENDING)"
+          echo "=== Python version ==="
+          python3 --version
+          echo "=== T27C_COMMIT ==="
+          echo "${T27C_COMMIT}"
+
+      - name: Create evidence directory
+        run: mkdir -p evidence
+
+      - name: Run EQY equivalence check
+        id: eqy_run
+        run: |
+          bash scripts/eqy_check.sh
+        continue-on-error: true
+
+      - name: Evaluate verdict (FAIL blocks, PENDING warns)
+        run: |
+          echo "=== Evidence files written ==="
+          ls -la evidence/eqy_*.json 2>/dev/null || echo "(no evidence files)"
+
+          # Parse verdicts from JSON evidence
+          FAIL_COUNT=0
+          PENDING_COUNT=0
+          PASS_COUNT=0
+
+          for f in evidence/eqy_*.json; do
+            if [[ -f "$f" ]]; then
+              MODULE=$(python3 -c "import json; print(json.load(open('$f'))['module'])")
+              VERDICT=$(python3 -c "import json; print(json.load(open('$f'))['verdict'])")
+              echo "  ${MODULE}: ${VERDICT}"
+              case "${VERDICT}" in
+                PASS)    PASS_COUNT=$((PASS_COUNT + 1)) ;;
+                FAIL)    FAIL_COUNT=$((FAIL_COUNT + 1)) ;;
+                PENDING) PENDING_COUNT=$((PENDING_COUNT + 1)) ;;
+              esac
+            fi
+          done
+
+          echo ""
+          echo "=== Summary ==="
+          echo "  PASS:    ${PASS_COUNT}"
+          echo "  PENDING: ${PENDING_COUNT}"
+          echo "  FAIL:    ${FAIL_COUNT}"
+          echo ""
+          echo "Anchor: phi^2 + phi^-2 = 3 · Wave-24 RVR-017"
+
+          # PENDING warning (R5-honest)
+          if [[ ${PENDING_COUNT} -gt 0 ]]; then
+            echo ""
+            echo "::warning::${PENDING_COUNT} module(s) are PENDING — t27c gen-verilog output"
+            echo "::warning::not yet committed to build/t27c/. See docs/EQY_CHECK.md for status."
+            echo "::warning::Set EQY_STRICT=1 in workflow env once build/t27c/*.v are committed."
+          fi
+
+          # FAIL is a hard blocker
+          if [[ ${FAIL_COUNT} -gt 0 ]]; then
+            echo "::error::${FAIL_COUNT} module(s) FAILED formal equivalence check."
+            echo "::error::Merge is BLOCKED until all modules pass EQY."
+            exit 1
+          fi
+
+          echo "EQY gate PASSED (no FAIL verdicts)."
+
+      - name: Upload evidence artifacts
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: eqy-evidence-${{ github.sha }}
+          path: evidence/eqy_*.json
+          retention-days: 90
+
+      - name: Generate GitHub Step Summary
+        if: always()
+        run: |
+          echo "## Yosys EQY Formal Equivalence — Wave-24 RVR-017" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "| Module | Verdict | t27c SHA | src SHA |" >> $GITHUB_STEP_SUMMARY
+          echo "|--------|---------|----------|---------|" >> $GITHUB_STEP_SUMMARY
+
+          for f in evidence/eqy_*.json; do
+            if [[ -f "$f" ]]; then
+              python3 - <<'PYEOF'
+          import json, sys, os
+          f = sys.argv[1] if len(sys.argv) > 1 else None
+          import glob
+          files = glob.glob('evidence/eqy_*.json')
+          for fp in sorted(files):
+              d = json.load(open(fp))
+              v = d['verdict']
+              icon = {'PASS': '✅', 'FAIL': '❌', 'PENDING': '⏳'}.get(v, '?')
+              t_sha = d.get('t27c_sha', 'MISSING')[:16] if d.get('t27c_sha') != 'MISSING' else 'MISSING'
+              s_sha = d.get('src_sha', 'MISSING')[:16]
+              print(f"| {d['module']} | {icon} {v} | {t_sha} | {s_sha} |")
+          PYEOF
+              break
+            fi
+          done >> $GITHUB_STEP_SUMMARY || true
+
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "**T27C_COMMIT:** \`${T27C_COMMIT}\`" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "> Anchor: \`phi^2 + phi^-2 = 3 · Wave-24 RVR-017 · DOI 10.5281/zenodo.19227877\`" >> $GITHUB_STEP_SUMMARY