From bfcbe3d62a27229df9f90c09e1f2ae6d623865f2 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Wed, 19 Aug 2026 23:37:52 +0700 Subject: [PATCH] ci(fpga)+fix: the vacuous greens are gates again Self-audit over the first full-green master run found three jobs that were green while verifying nothing, each confirmed by two independent refutation passes. fpga-formal: .sby files used indented pseudo-blocks sby does not parse (the bmc task saw no [engines] and died before any solver), [files] paths escaped the workspace, the 'if sby|tee' tested tee without pipefail so PASS was unconditional, and continue-on-error capped the job green over everything. fpga-conformance: bare -g2005 compiled 0 of 32 testbenches and the failure was a warning; the 'CLEAN' verdict in the summary is a static JSON field echoed as if computed (vvp lane: #2241). fpga-lint: the repo's own readiness tool printed NOT READY and exited 0; 1/32 invalid Verilog was a warning. All four now fail when they find nothing: canonical per-line sby task conditionals with local paths, pipefail + no continue-on-error + FAIL fails the step, -g2012 -DSIMULATION + exit 1, lint exit 1, synth-readiness bails on NOT READY. The expected honest red on lint has a named cause: a live gen-verilog regression (#2240) that the warning-gate absorbed within 40 minutes of the 32/32 claim. Closes #2239. --- .github/workflows/fpga-build.yml | 22 +++++++++++++++++----- bootstrap/src/main.rs | 4 ++++ contrib/formal/fifo_formal.sby | 18 ++++++++++-------- contrib/formal/mac_formal.sby | 22 +++++++++++++--------- contrib/formal/uart_formal.sby | 10 +++++----- docs/NOW.md | 21 +++++++++++++++++++++ 6 files changed, 70 insertions(+), 27 deletions(-) diff --git a/.github/workflows/fpga-build.yml b/.github/workflows/fpga-build.yml index 0156877327..e818e974a2 100644 --- a/.github/workflows/fpga-build.yml +++ b/.github/workflows/fpga-build.yml @@ -163,7 +163,11 @@ jobs: total=$((pass+fail)) echo "**Result:** $pass/$total modules passed Yosys lint" >> $GITHUB_STEP_SUMMARY if [ "$fail" -gt 0 ]; then - echo "::warning::$fail/$total modules failed Yosys lint" + # Audit 2026-08-19: a warning-only gate absorbed a live codegen + # regression (fifo.v invalid Verilog) within 40 minutes of the + # 32/32 claim. Lint failures now fail the step. + echo "::error::$fail/$total modules failed Yosys lint" + exit 1 fi fpga-synthesis: @@ -522,7 +526,6 @@ jobs: timeout-minutes: 45 needs: fpga-smoke runs-on: ubuntu-latest - continue-on-error: true steps: - uses: actions/checkout@v6 @@ -578,6 +581,9 @@ jobs: echo "" >> $GITHUB_STEP_SUMMARY echo "| Module | Solver | Task | Result |" >> $GITHUB_STEP_SUMMARY echo "|--------|--------|------|--------|" >> $GITHUB_STEP_SUMMARY + # Audit 2026-08-19: without pipefail the if tested tee's exit (always 0), + # so PASS was recorded unconditionally and the FAIL branch was unreachable. + 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 @@ -590,9 +596,12 @@ jobs: echo "| $module_name | Z3 | BMC+prove | PASS |" >> $GITHUB_STEP_SUMMARY else echo "| $module_name | Z3 | BMC+prove | FAIL/UNKNOWN |" >> $GITHUB_STEP_SUMMARY - echo "::warning::Formal verification of $module_name did not pass" + echo "::error::Formal verification of $module_name did not pass" + formal_failed=1 fi done + # A refusal on the record beats a vacuous green (repo doctrine, NOW.md). + [ "${formal_failed:-0}" = "1" ] && exit 1 else echo "| (all) | SymbiYosys not installed | - | SKIPPED |" >> $GITHUB_STEP_SUMMARY echo "::warning::SymbiYosys (sby) not available, formal check skipped" @@ -690,7 +699,9 @@ jobs: # has non-constant args synthesis cannot evaluate (mac.v:535). As # written, this loop could never have passed. name=$(sed -n 's/^module \([A-Za-z0-9_]*\).*/\1/p' "$v" | head -1) - if iverilog -o "build/fpga/conformance/${name}_tb.vvp" -g2005 "$v" 2>/dev/null; then + # Audit 2026-08-19: bare -g2005 compiled 0/32 -- the repo convention + # (-sv -DSIMULATION, same fix as the yosys loop) was never applied here. + if iverilog -o "build/fpga/conformance/${name}_tb.vvp" -g2012 -DSIMULATION "$v" 2>/dev/null; then pass=$((pass+1)) else fail=$((fail+1)) @@ -704,7 +715,8 @@ jobs: echo "| Total | $total |" >> $GITHUB_STEP_SUMMARY echo "" >> $GITHUB_STEP_SUMMARY if [ "$fail" -gt 0 ]; then - echo "::warning::$fail/$total modules failed iverilog compilation" + echo "::error::$fail/$total modules failed iverilog compilation" + exit 1 fi - name: Validate conformance JSON structure diff --git a/bootstrap/src/main.rs b/bootstrap/src/main.rs index 2a05e5e75d..af7acfc532 100644 --- a/bootstrap/src/main.rs +++ b/bootstrap/src/main.rs @@ -10469,6 +10469,10 @@ fn run_synth_readiness(specs_dir: &str) -> anyhow::Result<()> { println!("\nALMOST READY — test coverage needs improvement"); } else { println!("\nNOT READY — fix parse/verilog errors first"); + // Audit 2026-08-19: this verdict printed for months while the step stayed + // green -- the binary always exited 0. A verdict that gates nothing is a + // caption, not a check. + anyhow::bail!("synth-readiness: NOT READY"); } Ok(()) diff --git a/contrib/formal/fifo_formal.sby b/contrib/formal/fifo_formal.sby index 9d09a36fda..52e28ee6d8 100644 --- a/contrib/formal/fifo_formal.sby +++ b/contrib/formal/fifo_formal.sby @@ -1,23 +1,25 @@ +# Audit 2026-08-19: the old file used indented pseudo-blocks after 'bmc:'/'prove:', +# which sby does not parse as task conditionals -- the bmc task saw no [engines] +# and died with 'Config file is lacking engine configuration' on every run. Task +# conditionals in sby are per-line 'task: option'. Paths were ../../../specs/fpga/ +# which escapes the workspace; the workflow copies the generated .v NEXT TO this file. [tasks] bmc prove [options] -bmc: - mode bmc - depth 30 -prove: - mode prove - depth 30 +bmc: mode bmc +prove: mode prove +depth 30 [engines] smtbmc z3 [script] -read_verilog -formal ../../../specs/fpga/fifo.v +read_verilog -formal fifo.v read_verilog fifo_formal_props.v prep -top fifo_formal_props [files] -../../../specs/fpga/fifo.v +fifo.v fifo_formal_props.v diff --git a/contrib/formal/mac_formal.sby b/contrib/formal/mac_formal.sby index 74177edb4c..70da0a1ab9 100644 --- a/contrib/formal/mac_formal.sby +++ b/contrib/formal/mac_formal.sby @@ -1,21 +1,25 @@ +# Audit 2026-08-19: the old file used indented pseudo-blocks after 'bmc:'/'prove:', +# which sby does not parse as task conditionals -- the bmc task saw no [engines] +# and died with 'Config file is lacking engine configuration' on every run. Task +# conditionals in sby are per-line 'task: option'. Paths were ../../../specs/fpga/ +# which escapes the workspace; the workflow copies the generated .v NEXT TO this file. [tasks] bmc prove [options] -bmc: - mode bmc - depth 20 -prove: - mode prove - depth 20 +bmc: mode bmc +prove: mode prove +depth 20 [engines] smtbmc z3 [script] -read_verilog -formal ../../../specs/fpga/mac.v -prep -top ZeroDSP_MAC +read_verilog -formal mac.v +read_verilog mac_formal_props.v +prep -top mac_formal_props [files] -../../../specs/fpga/mac.v +mac.v +mac_formal_props.v diff --git a/contrib/formal/uart_formal.sby b/contrib/formal/uart_formal.sby index 16cdbed9c3..ae69291183 100644 --- a/contrib/formal/uart_formal.sby +++ b/contrib/formal/uart_formal.sby @@ -1,19 +1,19 @@ +# Audit 2026-08-19: see fifo_formal.sby header -- same two defects fixed. [tasks] bmc [options] -bmc: - mode bmc - depth 50 +mode bmc +depth 50 [engines] smtbmc z3 [script] -read_verilog -formal ../../../specs/fpga/uart.v +read_verilog -formal uart.v read_verilog uart_formal_props.v prep -top uart_formal_props [files] -../../../specs/fpga/uart.v +uart.v uart_formal_props.v diff --git a/docs/NOW.md b/docs/NOW.md index ef602c992c..365d9d11ca 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,24 @@ +# NOW -- the vacuous greens are gates again (2026-08-19) + +Last updated: 2026-08-19 + +## ci(fpga)+fix: formal/conformance/lint/readiness now fail when they find nothing (Closes #2239) + +- Adversarial self-audit over the green master run (each finding survived two + independent refutation passes): fpga-formal verified ZERO properties (sby + pseudo-block configs + workspace-escaping paths + missing pipefail + a + continue-on-error cap -- three independent layers each guaranteeing green); + fpga-conformance compiled 0/32 (bare -g2005) behind a warning, and never runs + vvp at all (#2241); fpga-lint absorbed 'NOT READY' and 1/32 invalid Verilog + as warnings +- Fixed: canonical per-line .sby task conditionals + local [files] paths; + set -o pipefail + continue-on-error removed + FAIL fails; iverilog -g2012 + -DSIMULATION + exit 1; lint exit 1; synth-readiness bails on NOT READY +- These jobs may now go honestly red on master: the lint red has a named cause + -- a live gen-verilog regression gluing a struct-field onto a part-select in + fifo.v (#2240), absorbed by the old warning-gate 40 minutes after the 32/32 + claim. A refusal on the record beats a vacuous green + # NOW -- the mismatch now fails where the cause is (2026-08-19) Last updated: 2026-08-19