From bfcbe3d62a27229df9f90c09e1f2ae6d623865f2 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Wed, 19 Aug 2026 23:37:52 +0700 Subject: [PATCH 1/2] 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 015687732..e818e974a 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 2a05e5e75..af7acfc53 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 9d09a36fd..52e28ee6d 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 74177edb4..70da0a1ab 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 16cdbed9c..ae6929118 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 ef602c992..365d9d11c 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 From d3474af8f2c7291dc17042f0823d1365c0296d64 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Wed, 19 Aug 2026 23:44:58 +0700 Subject: [PATCH 2/2] fix(gen-verilog): nested scalar-struct field access resolves to one cumulative part-select state.flags.empty emitted 'state[96 +: 4]_empty' -- the ExprFieldAccess branch matched identifier, index and call bases but not a field-access base, so the chain fell through to name-flattening and glued an identifier fragment onto a part-select (fifo.v, 6 sites, invalid Verilog live on master; absorbed for 40 minutes by the old warning-only lint gate). The chain now resolves to a single cumulative part-select: state[96 +: 1] for flags.empty, state[97 +: 1] for flags.full. Signed fields keep the $signed() wrap on rvalue reads. M5 performed. Negative controls: zero glued sites in regenerated fifo.v; yosys parses it; the full 32-module smoke set lints 32/32 with the repo's own flags. Closes #2240. --- bootstrap/src/compiler.rs | 60 ++++++++++++++++++++++++++++++++++++ bootstrap/stage0/FROZEN_HASH | 2 +- docs/NOW.md | 17 ++++++++++ 3 files changed, 78 insertions(+), 1 deletion(-) diff --git a/bootstrap/src/compiler.rs b/bootstrap/src/compiler.rs index d5399ce29..b56090f21 100644 --- a/bootstrap/src/compiler.rs +++ b/bootstrap/src/compiler.rs @@ -15044,6 +15044,66 @@ impl VerilogCodegen { return; } let child = &node.children[0]; + // #2240: NESTED scalar-struct field access (e.g. state.flags.empty). + // The single-level branch below matches only identifier/index/call + // bases, so a field-access base fell through to name-flattening and + // emitted `state[96 +: 4]_empty` -- an identifier fragment glued onto + // a part-select, invalid Verilog (fifo.v, 6 sites). Resolve the whole + // chain to ONE cumulative part-select on the base identifier. + if child.kind == NodeKind::ExprFieldAccess { + let mut names = vec![node.name.clone()]; + let mut cur = child; + while cur.kind == NodeKind::ExprFieldAccess && !cur.children.is_empty() { + names.push(cur.name.clone()); + cur = &cur.children[0]; + } + if cur.kind == NodeKind::ExprIdentifier { + names.reverse(); + let chain_base = cur.name.clone(); + if let Some(local_ty) = self.local_types + .get(&chain_base) + .or_else(|| self.param_types.get(&chain_base)) + .or_else(|| self.module_types.get(&chain_base)) + { + if self.is_lowerable_scalar_struct_type(local_ty) + && Self::parse_array_type(local_ty).is_none() + { + let mut cur_ty = Self::base_type_name(local_ty); + let mut total_off = 0u32; + let mut fw = 0u32; + let mut ftype = String::new(); + let mut ok = true; + for fname in &names { + match self.struct_field_offset(&cur_ty, fname) { + Some((off, w)) => { + total_off += off; + fw = w; + ftype = self.struct_decls.get(&cur_ty) + .and_then(|fs| { + fs.iter() + .find(|(n, _)| n == fname) + .map(|(_, t)| t.clone()) + }) + .unwrap_or_default(); + cur_ty = Self::base_type_name(&ftype); + } + None => { ok = false; break; } + } + } + if ok && fw > 0 { + let signed = Self::scalar_field_is_signed(&ftype); + let slice = format!("{}[{} +: {}]", chain_base, total_off, fw); + if signed && !self.in_lvalue { + self.write(&format!("$signed({})", slice)); + } else { + self.write(&slice); + } + return; + } + } + } + } + } // W533: packed single scalar-struct field access (e.g. p.x). let base_name = match child.kind { NodeKind::ExprIdentifier => child.name.clone(), diff --git a/bootstrap/stage0/FROZEN_HASH b/bootstrap/stage0/FROZEN_HASH index a0232017d..8f0ec1b67 100644 --- a/bootstrap/stage0/FROZEN_HASH +++ b/bootstrap/stage0/FROZEN_HASH @@ -1 +1 @@ -54d19991b0c234c95d83d5348d546f4d91b2732b39bea29f8d4459e4cc248ba2 +375b2f88cc2f1c58e5ec26bae8efd1f78fa712491a98216cfd98a69d206ae041 diff --git a/docs/NOW.md b/docs/NOW.md index 365d9d11c..d5b7a530f 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,20 @@ +# NOW -- the honest red has been repaired for real (2026-08-20) + +Last updated: 2026-08-20 + +## fix(gen-verilog): nested struct field resolves to one cumulative part-select (Closes #2240) + +- state.flags.empty emitted 'state[96 +: 4]_empty' -- the ExprFieldAccess branch + matched identifier/index/call bases but not a field-access base, so the chain + fell through to name-flattening and glued an identifier onto a part-select + (fifo.v, 6 sites, invalid Verilog; the old warning-only lint absorbed it for + 40 minutes after the 32/32 claim) +- The chain now resolves to a single cumulative part-select (state[96 +: 1] / + state[97 +: 1]); signed fields keep $signed() on rvalue reads. M5 performed +- Negative controls: zero glued sites in regenerated fifo.v; yosys parses it; + the full 32-module smoke set lints 32/32 with the repo's own flags -- the + honest lint gate (#2239) can now be GREEN for real + # NOW -- the vacuous greens are gates again (2026-08-19) Last updated: 2026-08-19