Skip to content

ci(formal): read the props file with -formal #2272

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gHashTag merged 1 commit into from
Aug 19, 2026
+14 −3
Merged

ci(formal): read the props file with -formal #2272

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion contrib/formal/fifo_formal.sby
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ smtbmc z3

[script]
read_verilog -formal -sv -DSIMULATION fifo.v
read_verilog fifo_formal_props.v
read_verilog -formal fifo_formal_props.v
prep -top fifo_formal_props

[files]
Expand Down
2 changes: 1 addition & 1 deletion contrib/formal/mac_formal.sby
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ smtbmc z3

[script]
read_verilog -formal -sv -DSIMULATION mac.v
read_verilog mac_formal_props.v
read_verilog -formal mac_formal_props.v
prep -top mac_formal_props

[files]
Expand Down
2 changes: 1 addition & 1 deletion contrib/formal/uart_formal.sby.blocked
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ smtbmc z3

[script]
read_verilog -formal -sv -DSIMULATION uart.v
read_verilog uart_formal_props.v
read_verilog -formal uart_formal_props.v
prep -top uart_formal_props

[files]
Expand Down
11 changes: 11 additions & 0 deletions docs/NOW.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,14 @@
# NOW -- the props read with -formal too (2026-08-20)

Last updated: 2026-08-20

## ci(formal): -formal on the props read line (Closes #2271)

- The layer-5 flag fix covered only the DUT line; CI yosys read the props
plain and resolved 'assert' as a task name (rc=16) while the local proof
had flagged both reads. Reproduced the exact CI error locally without the
flag; with it the chain proves Status PASSED. One line per .sby

# NOW -- the first real formal verdicts: fifo and mac PROVE (2026-08-20)

Last updated: 2026-08-20
Expand Down
Loading