Introduce an OSS Formal Flow #2309

mndstrmr · 2025-08-20T16:15:10Z

This PR introduces a formal flow for Ibex that does not depend on Jasper, instead using yosys and our fork of the yosys-slang frontend to produce an aiger file, which the rIC3 model checker, under the instruction of conductor.py, can then verify. Just one aiger file is created, and is subsequently reconfigured by the Rust aig-manip tool.

This commit also introduces a new ci job which invokes the OS formal flow. It uses the nix flake, which contains all the necessary dependencies.

See dv/formal/README.md for more details, but in general:

We generate the specification module and psgen RTL in roughly the same way as the Jasper flow, with small changes to the psgen output in particular.
We use a fork of yosys-slang as the frontend for yosys. It has comprehensive SystemVerilog support, and handles both the specification and Ibex easily. It lacks SVA support by default, hence the need for the fork, though hopefully this will be upstreamed soon. The RTL source list is constructed by fusesoc in the same way as for Jasper.
The yosys build script is then specified in build_all.ys. It makes use of three custom passes, which may be found in yosys_formal. See their source files for more explanation of what they do. Yosys takes ~10 minutes to build an aiger file. See aig-manip/src/main.rs for more description of aiger files.
In order to prove a property, the rIC3 model checker can be used. However, the aiger file produced by yosys in step 3 contains all properties as assertions. To focus on just one, and to take all prior steps as assumptions the aig-manip tool is used. After this invocation of rIC3 is straightforward for IC3, k-induction or BMC. If a CEX is discovered it may be analysed by the aig-manip tool, which can lift the AIW (aiger witness) into a VCD file, for use in gtkwave etc.
When considering the proof as a whole, the conductor.py script is used to discover proof strategies, and then run proofs while maximising memory usage. It caches proofs for each step under strategies/step*.json.

Additonal notes:

The actual proof is relatively unchanged, with just a couple of new properties.
The proof is fast (it takes 40 minutes or so in CI)
smt2 based proofs are also available, e.g. for k-induction, since the build script (build_all.ys) will produce an smt2 file, which can be manipulated by smt2manip.py in the same that aig-manip does for an aiger file.
The transformation made to a global clock will confuse clock gating. It should be fine, since the clock signal it generates is essentially ignored anyway.

marnovandermaas

It would be nice to split the formal fixing changes from the open source flow (as you suggested in person). Here are just a few comments based on an initial read though. Todo for me is read through conductor.py and aig-manip

dv/formal/strategies/step0.json

dv/formal/spec/spec_api.sv

dv/formal/check/top.sv

dv/formal/check/protocol/mem.sv

dv/formal/yosys_formal/compile_flags.txt

marnovandermaas

Looks like you need to run a clang format and a Verible lint to make CI happy.

marnovandermaas

Just reviewing conductor.py
Really cool stuff and some comments for you to address while we get more feedback.

dv/formal/conductor.py

dv/formal/aig-manip/src/bitvec.rs

machshev

Nice work! Some nits...

dv/formal/spec/fix_bugs.py

dv/formal/conductor.py

machshev · 2025-09-03T11:24:50Z

dv/formal/smt2manip.py

+        step = int(step[4:])
+
+        if name.endswith("_Cover") or step > args.step or (step == args.step and len(args.props) > 0 and name not in args.props):
+            print(f"Delete {name} ({id})")


Generally preferable to use log.info instead of print for massages you always want to see. Alternatively log.debug for messages that should only show in verbose mode.

dv/formal/smt2manip.py

dv/formal/conductor.py

marnovandermaas

Left a few comments. I still need to run the flow again before I approve.

dv/formal/thm/riscv.proof

.github/workflows/ci-formal.yml

marnovandermaas

This proof ran through to me so I am happy to approve it. I would like at least one other person to approve this before we merge, this can be @nbdd0121 @hcallahan-lowrisc @machshev or @jwnrt .
The only thing that I can currently think of that would be good is to change the maximum memory to half of the total in Pomona.

jwnrt

Briefly reviewed the Rust and didn't see any problems, LGTM

hcallahan-lowrisc

This looks great. I'm super happy to see this get merged. Well done @mndstrmr for all the great work!

One note before merging. Some files seem to be missing copyright/license headers. @marnovandermaas would you mind going through all the formal files and checking?

flake.nix

yosys.nix

dv/formal/Makefile

hcallahan-lowrisc · 2025-09-19T10:31:52Z

dv/formal/Makefile

+
+# The aiger file for the OSS flow, using the yosys_formal/* plugins. The main yosys script is in build_all.ys
+build/all.aig: build/psgen-yosys.sv build/fusesoc build/ibexspec.sv check build_all.ys $(LOWRISC_YOSYS_SLANG) build/yosys_formal.so
+	yosys -m $(LOWRISC_YOSYS_SLANG) -m build/yosys_formal.so -v 1 -s <(cat ./build_all.ys | sed "s|LOWRISC_SAIL_SRC|$(LOWRISC_SAIL_SRC)|g")


Slightly annoying yosys can't do environment variable substitution, would be nice to not have to do this dance with sed.

It unfortunate. Even using envsubst won't work due to this line:

ibex/dv/formal/build_all.ys

Line 18 in eb6e0ac

delete */t:$print

You might be able to turn build_all.ys into a Tcl script and look up the environment via $::env(FOO). Yosys has an embedded Tcl interpreter in most builds

mndstrmr · 2025-09-19T12:02:45Z

This proof ran through to me so I am happy to approve it. I would like at least one other person to approve this before we merge, this can be @nbdd0121 @hcallahan-lowrisc @machshev or @jwnrt . The only thing that I can currently think of that would be good is to change the maximum memory to half of the total in Pomona.

It's nice to see that halving the memory does in fact double the runtime, as expected. 200GB does 43 minutes, 100GB did 81 minutes. See this run.

jwnrt · 2025-09-19T12:34:29Z

Nice, 80m is still within my personal comfortable range for a PR workflow given that it's not blocking or in the merge queue.

.github/workflows/ci-formal.yml

mndstrmr · 2025-09-19T14:26:22Z

That should be the final force push (a missing license header in Cargo.toml) done now.

buildspec.py previously allowed us to cut out specific instructions from the specification, this allowed for faster build times and so a tighter feedback loop. Now, building and elaborating the Sail specification is fast enough that this is no longer necessary. We can therefore remove `ISS_instr and {ex,wbexc}_is_pres_instr, as weel as instrs.json. Also renames Sources.mk to sail-sources.mk for clarity.

Previously we used -fun2wires 2:rX so that we could track which registers were being used. This was leading to combinational loops, and so had already been removed from CHERIoT-Ibex. We can still 'track' them using Ibex's own interpretation of which registers are relevant, and marking the rest as x.

Yosys-slang is a SystemVerilog frontend to yosys, which will be used in upcoming formal work. It takes issue with some parts of the formal flow. This commit cleans things up so that it may consume the RTL happily.

This commit introduces a formal flow for Ibex that does not depend on Jasper, instead using yosys and our fork of the yosys-slang frontend to produce an aiger file, which the rIC3 model checker, under the instruction of conductor.py, can then verify. Just one aiger file is created, and is subsequently reconfigured by the Rust aig-manip tool. See dv/formal/README.md for more details, but in general: 1. We generate the specification module and psgen RTL in roughly the same way as the Jasper flow, with small changes to the psgen output in particular. 2. We use a fork of yosys-slang as the frontend for yosys. It has comprehensive SystemVerilog support, and handles both the specification and Ibex easily. It lacks SVA support by default, hence the need for the fork, though hopefully this will be upstreamed soon. The RTL source list is constructed by fusesoc in the same way as for Jasper. 3. The yosys build script is then specified in build_all.ys. It makes use of three custom passes, which may be found in yosys_formal. See their source files for more explanation of what they do. Yosys takes ~10 minutes to build an aiger file. See aig-manip/src/main.rs for more description of aiger files. 4. In order to prove a property, the rIC3 model checker can be used. However, the aiger file produced by yosys in step 3 contains all properties as assertions. To focus on just one, and to take all prior steps as assumptions the aig-manip tool is used. After this invocation of rIC3 is straightforward for IC3, k-induction or BMC. If a CEX is discovered it may be analysed by the aig-manip tool, which can lift the AIW (aiger witness) into a VCD file, for use in gtkwave etc. 5. When considering the proof as a whole, the conductor.py script is used to discover proof strategies, and then run proofs while maximising memory usage. It caches proofs for each step under strategies/step*.json. Additonal notes: 1. The actual proof is relatively unchanged, with just a couple of new properties. 2. The proof is fast (it takes 40 minutes or so on a good machine) 3. smt2 based proofs are also available, e.g. for k-induction, since the build script (build_all.ys) will produce an smt2 file, which can be manipulated by smt2manip.py in the same that aig-manip does for an aiger file. 4. The transformation made to a global clock will confuse clock gating. It *should* be fine, since the clock signal it generates is essentially ignored anyway. 5. This commit also switches from poetry to UV. 6. This runs on a small memory bound (the smallest possible bound). See check/protocol/mem.sv

This commit introduces a new ci job which invokes the OS formal flow. It uses the nix flake, which contains all the necessary dependencies. With everything already in cache this takes less than an hour on pomona. A parameter (MAX_MEM_GB) can be used to limit memory usage.

mndstrmr requested review from marnovandermaas and nbdd0121 August 20, 2025 16:15

mndstrmr marked this pull request as draft August 20, 2025 16:15

marnovandermaas reviewed Aug 21, 2025

View reviewed changes

mndstrmr force-pushed the oss-formal branch 2 times, most recently from 32dd8e2 to ff5bcef Compare August 21, 2025 09:37

mndstrmr requested a review from hcallahan-lowrisc August 21, 2025 09:41

mndstrmr force-pushed the oss-formal branch 2 times, most recently from 780fde9 to fad268c Compare August 21, 2025 09:57

marnovandermaas reviewed Sep 2, 2025

View reviewed changes

marnovandermaas reviewed Sep 3, 2025

View reviewed changes

dv/formal/aig-manip/src/bitvec.rs Show resolved Hide resolved

machshev reviewed Sep 3, 2025

View reviewed changes

mndstrmr force-pushed the oss-formal branch 11 times, most recently from 34d04aa to 5c4f560 Compare September 18, 2025 09:27

mndstrmr marked this pull request as ready for review September 18, 2025 09:28

marnovandermaas reviewed Sep 18, 2025

View reviewed changes

dv/formal/thm/riscv.proof Show resolved Hide resolved

.github/workflows/ci-formal.yml Outdated Show resolved Hide resolved

.github/workflows/ci-formal.yml Show resolved Hide resolved

marnovandermaas approved these changes Sep 19, 2025

View reviewed changes

jwnrt approved these changes Sep 19, 2025

View reviewed changes

mndstrmr force-pushed the oss-formal branch from 5c4f560 to 7c9b433 Compare September 19, 2025 10:14

hcallahan-lowrisc approved these changes Sep 19, 2025

View reviewed changes

mndstrmr force-pushed the oss-formal branch 2 times, most recently from 5427262 to eb6e0ac Compare September 19, 2025 11:07

jwnrt reviewed Sep 19, 2025

View reviewed changes

.github/workflows/ci-formal.yml Show resolved Hide resolved

mndstrmr force-pushed the oss-formal branch from eb6e0ac to 14aef04 Compare September 19, 2025 14:24

mndstrmr added 5 commits September 19, 2025 15:34

[dv/formal] Cleanup RTL for use by yosys-slang

b10eedb

Yosys-slang is a SystemVerilog frontend to yosys, which will be used in upcoming formal work. It takes issue with some parts of the formal flow. This commit cleans things up so that it may consume the RTL happily.

mndstrmr force-pushed the oss-formal branch from 14aef04 to 4293c3c Compare September 19, 2025 14:34

marnovandermaas added this pull request to the merge queue Sep 19, 2025

Merged via the queue into master with commit 1f2232a Sep 19, 2025
13 checks passed

marnovandermaas mentioned this pull request Sep 19, 2025

[dv] Formal flow dependency #2321

Open

povik mentioned this pull request Oct 17, 2025

SVA (SystemVerilog assertions) support povik/yosys-slang#77

Open

Introduce an OSS Formal Flow #2309

Introduce an OSS Formal Flow #2309

Uh oh!

Conversation

mndstrmr commented Aug 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

marnovandermaas left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

marnovandermaas left a comment

Choose a reason for hiding this comment

Uh oh!

marnovandermaas left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

machshev left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

machshev Sep 3, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

marnovandermaas left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

marnovandermaas left a comment

Choose a reason for hiding this comment

Uh oh!

jwnrt left a comment

Choose a reason for hiding this comment

Uh oh!

hcallahan-lowrisc left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hcallahan-lowrisc Sep 19, 2025

Choose a reason for hiding this comment

Uh oh!

mndstrmr Sep 19, 2025

Choose a reason for hiding this comment

Uh oh!

povik Sep 21, 2025

Choose a reason for hiding this comment

Uh oh!

mndstrmr commented Sep 19, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jwnrt commented Sep 19, 2025

Uh oh!

Uh oh!

mndstrmr commented Sep 19, 2025

mndstrmr commented Aug 20, 2025 •

edited

Loading

mndstrmr commented Sep 19, 2025 •

edited

Loading