From cc297fb6d7b0bba1725829321fcd08409fc31108 Mon Sep 17 00:00:00 2001
From: Vasilev Dmitrii <raoffonom@icloud.com>
Date: Thu, 20 Aug 2026 05:57:14 +0700
Subject: [PATCH] ci(fpga): formal prefers the RTL it just generated over stale
 committed copies

Formal layer 6: the copy chain preferred committed specs/fpga/*.v --
April-14 vintage with same-line translate_off comments the current
emitter no longer writes -- over the artifact generated minutes earlier
in the same run, so sby died on TOK_INITIAL in RTL four months older
than the compiler under test. Fresh generated first; stale fallback is
a loud warning; absence is fatal.

Closes #2261.
---
 .github/workflows/fpga-build.yml | 19 ++++++++++++++++---
 docs/NOW.md                      | 15 +++++++++++++++
 2 files changed, 31 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/fpga-build.yml b/.github/workflows/fpga-build.yml
index 86ef49dc8..132e9a449 100644
--- a/.github/workflows/fpga-build.yml
+++ b/.github/workflows/fpga-build.yml
@@ -590,9 +590,22 @@ jobs:
           set -o pipefail
           if command -v sby &>/dev/null; then
             cp -r contrib/formal build/fpga/formal
-            cp specs/fpga/mac.v build/fpga/formal/ 2>/dev/null || cp build/fpga/generated/mac.v build/fpga/formal/ 2>/dev/null || true
-            cp specs/fpga/fifo.v build/fpga/formal/ 2>/dev/null || cp build/fpga/generated/fifo.v build/fpga/formal/ 2>/dev/null || true
-            cp specs/fpga/uart.v build/fpga/formal/ 2>/dev/null || cp build/fpga/generated/uart.v build/fpga/formal/ 2>/dev/null || true
+            # FRESH generated RTL first: specs/fpga/*.v are April-vintage committed
+            # copies (translate_off comments the current emitter no longer writes)
+            # and shadowed the just-built artifact -- sby then died on TOK_INITIAL
+            # in RTL four months older than the compiler that was supposedly under
+            # test. Stale fallback is loud; absence is fatal.
+            for m in mac fifo uart; do
+              if [ -f "build/fpga/generated/${m}.v" ]; then
+                cp "build/fpga/generated/${m}.v" build/fpga/formal/
+              elif [ -f "specs/fpga/${m}.v" ]; then
+                echo "::warning::formal uses STALE committed specs/fpga/${m}.v (generated artifact missing)"
+                cp "specs/fpga/${m}.v" build/fpga/formal/
+              else
+                echo "::error::no ${m}.v available for formal (neither generated nor committed)"
+                exit 1
+              fi
+            done
             for sby_file in build/fpga/formal/*.sby; do
               module_name=$(basename "$sby_file" .sby)
               echo "Running formal: $module_name"
diff --git a/docs/NOW.md b/docs/NOW.md
index 268162fe0..863939e1e 100644
--- a/docs/NOW.md
+++ b/docs/NOW.md
@@ -1,3 +1,18 @@
+# NOW -- formal now tests the RTL it just built (2026-08-20)
+
+Last updated: 2026-08-20
+
+## ci(fpga): fresh generated RTL preferred over April-vintage committed copies (Closes #2261)
+
+- Formal layer 6, the real one behind the surviving TOK_INITIAL: the copy chain
+  preferred committed specs/fpga/{mac,fifo,uart}.v -- April-14 vintage, with
+  same-line translate_off comments the current emitter no longer writes -- over
+  the artifact generated minutes earlier in the same run. yosys hot-comment
+  skipping consumes the matching 'end', so the next initial is a syntax error
+- The chain now prefers build/fpga/generated/*.v, warns loudly on a stale
+  fallback, and fails when neither exists. The 30 stale committed .v files
+  under specs/fpga are an owner question (#2261), not a unilateral deletion
+
 # NOW -- the formal configs are visible to their own CI (2026-08-20)
 
 Last updated: 2026-08-20