From 23a7d25b0c2313e1f51c16a6420117a87685068e Mon Sep 17 00:00:00 2001
From: Vasilev Dmitrii <raoffonom@icloud.com>
Date: Thu, 20 Aug 2026 05:17:37 +0700
Subject: [PATCH] ci(fpga): invoke sby from the formal dir -- [files] resolve
 against cwd

Third formal layer: sby copies [files] entries relative to the invocation
cwd, not the .sby location, so all three tasks died on FileNotFoundError
while their .v files sat next to the configs (run 32305304787). The honest
gate recorded FAIL and failed the step exactly as designed. sby now runs
from build/fpga/formal via a subshell; pipefail is inherited.

Closes #2254.
---
 .github/workflows/fpga-build.yml |  4 +++-
 docs/NOW.md                      | 16 ++++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/fpga-build.yml b/.github/workflows/fpga-build.yml
index e818e974a..a56d42087 100644
--- a/.github/workflows/fpga-build.yml
+++ b/.github/workflows/fpga-build.yml
@@ -592,7 +592,9 @@ jobs:
             for sby_file in build/fpga/formal/*.sby; do
               module_name=$(basename "$sby_file" .sby)
               echo "Running formal: $module_name"
-              if sby -f "$sby_file" 2>&1 | tee "build/fpga/formal/${module_name}.log"; then
+              # sby resolves [files] against the INVOCATION cwd, not the .sby
+              # location -- run from the formal dir so local paths bind.
+              if (cd build/fpga/formal && sby -f "${module_name}.sby" 2>&1 | tee "${module_name}.log"); then
                 echo "| $module_name | Z3 | BMC+prove | PASS |" >> $GITHUB_STEP_SUMMARY
               else
                 echo "| $module_name | Z3 | BMC+prove | FAIL/UNKNOWN |" >> $GITHUB_STEP_SUMMARY
diff --git a/docs/NOW.md b/docs/NOW.md
index 3d3eb99f9..d31f85586 100644
--- a/docs/NOW.md
+++ b/docs/NOW.md
@@ -1,3 +1,19 @@
+# NOW -- sby runs from where its files are (2026-08-20)
+
+Last updated: 2026-08-20
+
+## ci(fpga): formal invokes sby from the formal dir (Closes #2254)
+
+- Third formal layer: sby resolves [files] against the invocation cwd, not the
+  .sby location -- all three tasks died on FileNotFoundError while their .v
+  files sat next to the configs. The honest gate recorded FAIL and failed the
+  step, exactly as designed. sby now runs from build/fpga/formal
+- Same run: fpga-lint GREEN for real (readiness 100%, 32/32 yosys after the
+  codegen fix); conformance honestly red -- 28/32 do not iverilog-compile, and
+  the classification (hierarchy elaboration + unbound flattened refs, mac.v:98
+  word_raw among them) is recorded in #2241: the job's premise must narrow to
+  vector-backed modules rather than chase meaningless RTL for config models
+
 # NOW -- readiness is READY, for real (2026-08-20)
 
 Last updated: 2026-08-20