ci(fpga): formal [script] reads with -sv -DSIMULATION

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
 

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
 

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
 

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