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