ci(fpga): formal prefers freshly generated RTL over stale committed copies

.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"

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