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