From 7131f21ecf175a1ec5ed1796afb4d54215fda7fc Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Thu, 20 Aug 2026 05:30:55 +0700 Subject: [PATCH] ci(fpga): formal [script] reads with -sv -DSIMULATION Formal layer 5: with the cwd fix in place sby ran its base yosys step for the first time in the job's history and died on fifo.v:369 TOK_INITIAL -- without -DSIMULATION the ifndef-guarded bench block (initial statements) survives into the formal read, and the emitter's SV static casts need -sv; every other Verilog reader in this repo already applies both flags. Verified locally: bare 'read_verilog -formal fifo.v' fails, with the flags it exits 0. Closes #2257. --- contrib/formal/fifo_formal.sby | 2 +- contrib/formal/mac_formal.sby | 2 +- contrib/formal/uart_formal.sby | 2 +- docs/NOW.md | 15 +++++++++++++++ 4 files changed, 18 insertions(+), 3 deletions(-) diff --git a/contrib/formal/fifo_formal.sby b/contrib/formal/fifo_formal.sby index 52e28ee6d..4070122c2 100644 --- a/contrib/formal/fifo_formal.sby +++ b/contrib/formal/fifo_formal.sby @@ -16,7 +16,7 @@ depth 30 smtbmc z3 [script] -read_verilog -formal fifo.v +read_verilog -formal -sv -DSIMULATION fifo.v read_verilog fifo_formal_props.v prep -top fifo_formal_props diff --git a/contrib/formal/mac_formal.sby b/contrib/formal/mac_formal.sby index 70da0a1ab..0687dfb84 100644 --- a/contrib/formal/mac_formal.sby +++ b/contrib/formal/mac_formal.sby @@ -16,7 +16,7 @@ depth 20 smtbmc z3 [script] -read_verilog -formal mac.v +read_verilog -formal -sv -DSIMULATION mac.v read_verilog mac_formal_props.v prep -top mac_formal_props diff --git a/contrib/formal/uart_formal.sby b/contrib/formal/uart_formal.sby index ae6929118..e761ec20d 100644 --- a/contrib/formal/uart_formal.sby +++ b/contrib/formal/uart_formal.sby @@ -10,7 +10,7 @@ depth 50 smtbmc z3 [script] -read_verilog -formal uart.v +read_verilog -formal -sv -DSIMULATION uart.v read_verilog uart_formal_props.v prep -top uart_formal_props diff --git a/docs/NOW.md b/docs/NOW.md index 985d2e5cc..b50c5e559 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,18 @@ +# NOW -- sby's yosys now reads the repo's own dialect (2026-08-20) + +Last updated: 2026-08-20 + +## ci(fpga): formal [script] gains -sv -DSIMULATION (Closes #2257) + +- Formal layer 5: with cwd fixed, sby ran its base yosys step for the first + time and died on fifo.v:369 TOK_INITIAL -- the bench block survives without + -DSIMULATION and SV casts need -sv, the same convention every other reader + in this repo already applies. Verified locally: bare read_verilog -formal + fails, with the flags it exits 0 +- Diagnosis route worth keeping: the engine failure is only named in the + fpga-formal ARTIFACT's per-task logfile.txt; the job log says merely + 'engine_0 did not return a status' + # NOW -- auto-merge-ready-prs.yml has not parsed since 2026-07-07 (2026-08-20) Last updated: 2026-08-20