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 83843a620e..9e4b59e0ed 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,25 @@ +# 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 tri CLI wave lands: mutate, pr ready, synth/sweep area (2026-08-20) Last updated: 2026-08-20