[dv/formal] Introduce an Open Source Formal Flow

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

Author: mndstrmr

.gitattributes

@@ -0,0 +1,4 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+dv/formal/strategies/* linguist-generated

Makefile

@@ -1,3 +1,7 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
 IBEX_CONFIG ?= small
 
 FUSESOC_CONFIG_OPTS = $(shell ./util/ibex_config.py $(IBEX_CONFIG) fusesoc_opts)

dv/formal/.gitignore

@@ -1,3 +1,4 @@
 build
 jgproject
 jgproofs
+aig-manip/target

dv/formal/Makefile

@@ -1,6 +1,12 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# Original author: Louis-Emile Ploix
+# SPDX-License-Identifier: Apache-2.0
+
 IBEX_ROOT=../..
 
-SAIL=sail
+SAIL=$(shell which sail)
+PSGEN=$(shell which psgen)
 
 SAIL_RISCV_MODEL_DIR=${LOWRISC_SAIL_RISCV_SRC}/model
 
@@ -9,7 +15,7 @@ include sail-sources.mk
 PSGEN_SRCS=thm/btype.proof thm/ibex.proof thm/mem.proof thm/riscv.proof
 PSGEN_FLAGS=-root riscv -task
 
-SAIL_EXTRA_SRCS=../spec/main.sail
+SAIL_EXTRA_SRCS=spec/main.sail
 
 # -sv, use the SystemVerilog backend
 # --sv-comb, generate a always_comb instead of an initial block
@@ -23,14 +29,14 @@ SAIL_SV_FLAGS=-sv --sv-comb --sv-inregs --sv-outregs --sv-nostrings --sv-nopacke
 	--sv-unreachable translate --sv-unreachable lookup_TLB --sv-unreachable translate_tlb_miss --sv-unreachable translate_tlb_hit --sv-unreachable pt_walk \
 	--sv-fun2wires 2:read_ram \
 	--sv-fun2wires 2:write_ram \
-	--sv-fun2wires wX 
+	--sv-fun2wires wX
 
 # Use fusesoc to resolve the tree of components, copy all resolved source files into the build/ directory,
 # and then generate a filelist for jasper to ingest.
 # - Note. we use the 'vcs' fusesoc backend flow to generate the filelist. This is because fusesoc does not currently implement a
-#   JasperGold backend, but this is not an issue as the file-format generated by the vcs flow is compatible with jasper.
-.PHONY: fusesoc
-fusesoc:
+#   JasperGold backend, but this is not an issue as the file-format generated by the vcs flow is compatible with both jasper and
+#   yosys-slang.
+build/fusesoc: $(IBEX_ROOT)/rtl $(IBEX_ROOT)/vendor
 	mkdir -p build/fusesoc
 	fusesoc \
 	  --cores-root $(IBEX_ROOT) \
@@ -39,33 +45,52 @@ fusesoc:
 	  --tool vcs \
 	  --setup \
 	  lowrisc:ibex:ibex_formal:0.1
+	touch build/fusesoc # Fix timestamps for Makefile
+
+# The sail spec module, constructed from LOWRISC_SAIL_RISCV_SRC, compiled by our fork of the sail compiler
+build/ibexspec.sv: $(SAIL) $(SAIL_SRCS) $(SAIL_EXTRA_SRCS) sail-sources.mk Makefile spec/fix_bugs.py
+	mkdir -p build
+	cd build && $(SAIL) $(SAIL_SRCS) $(addprefix ../,$(SAIL_EXTRA_SRCS)) $(SAIL_SV_FLAGS) $(addprefix -sv_unreachable execute_,$(COMPRESSED_INSTRS)) -o ibexspec
+	python3 spec/fix_bugs.py
+
+# The compiled property structure, and the associated TCL
+build/psgen-jg.sv: $(PSGEN) $(PSGEN_SRCS) Makefile
+	mkdir -p build
+	$(PSGEN) $(addprefix -path ,$(PSGEN_SRCS)) $(PSGEN_FLAGS) -sv-out build/psgen-jg.sv -tcl-out build/psgen.tcl
 
-.PHONY: sv
-sv:
+# Same as above, but generate our own covers, and tweak for consumption by our tools
+build/psgen-yosys.sv: $(PSGEN) $(PSGEN_SRCS) Makefile
 	mkdir -p build
-	python3 buildspec.py header > build/ibexspec_instrs.sv
-	cd build && $(SAIL) $(SAIL_SRCS) $(SAIL_EXTRA_SRCS) $(SAIL_SV_FLAGS) `cd .. && python3 buildspec.py unreachables` -o ibexspec
-	python3 spec/fix_pmp_bug.py
-	python3 buildspec.py unreachable_loc_hack
+	$(PSGEN) $(addprefix -path ,$(PSGEN_SRCS)) $(PSGEN_FLAGS) -sv-out build/psgen-yosys.sv -clocking -covers -cover-assert -step-prefix
+
+# 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")
 
-.PHONY: psgen
-psgen:
+# Build the custom yosys plugins
+build/yosys_formal.so: yosys_formal/global_clock.cc yosys_formal/write_aiger.cc yosys_formal/opt_muxtree.cc
+	yosys-config --build build/yosys_formal.so yosys_formal/global_clock.cc yosys_formal/write_aiger.cc yosys_formal/opt_muxtree.cc
+
+# Build the aig-manip Rust tool
+build/aig-manip: aig-manip/src/main.rs
 	mkdir -p build
-	psgen $(addprefix -path ,$(PSGEN_SRCS)) $(PSGEN_FLAGS) -sv-out build/psgen.sv -tcl-out build/psgen.tcl
+	cd aig-manip && cargo build --release
+	cp aig-manip/target/release/aig-manip build/
 
+# Run the jasper environment in interactive mode
 .PHONY: jg
-jg: fusesoc psgen sv
+jg: build/fusesoc build/psgen-jg.sv build/ibexspec.sv
 	jg verify.tcl -allow_unsupported_OS -acquire_proj
 
-# The following default target is intended for regressions / unattended runs.
+# Jasper environment for regression and unattended runs
 .PHONY: all
-all: fusesoc psgen sv
+all: build/fusesoc build/psgen-jg.sv build/ibexspec.sv
 	jg verify.tcl -allow_unsupported_OS -acquire_proj -no_gui --- "prove_no_liveness"
 
 ################################################################################
 
 .PHONY: clean
 clean:
-	rm -rf build/
-	rm -rf jgproject/
-	rm -rf jgproofs/
+	rm -rf build/ aig-manip/target
+	rm -rf jgproject/ jgproofs/
+

dv/formal/README.md

@@ -12,7 +12,7 @@ Getting started:
 - `cd dv/formal`
 
 ### Reproducible Build
-
+#### With Jasper:
 This flow is intended for users who wish to run the formal flow as-is using the pinned external dependencies (psgen, sail, riscv-sail etc.)
 
 Build instructions:
@@ -28,13 +28,22 @@ Some steps require a lot of RAM and CPU so we recommend closing any other resour
 A machine with 128 GiB of RAM and 32 cores was used to complete the proof.
 To avoid manually running each step you can also use the `prove_lemmas` command inside the TCL command interface located below your session window.
 
+#### With Yosys and rIC3:
+This is equivalent to the above, but uses only open source tools.
+
+Build instructions:
+- `nix develop .#oss-dev`
+- `make build/aig-manip` builds the Rust aig-manip tool used by conductor.py
+- `make build/all.aig` builds the core Aiger file
+- `python3 conductor.py prove` runs the proof, maximising memory usage. See `python3 conductor.py -h` for more options.
+
 ### Development Builds
 
 Users who wish to do development on this flow should use the below steps.
 This will allow changes to both the local files and the external dependencies (psgen, sail, riscv-sail), and to run the intermediate build steps manually.
 
-Build instructions:
-- Identical to the Reproducible Build steps, but use `nix develop .#formal-dev`.
+- For Jasper: Identical to the Reproducible Build steps, but use `nix develop .#formal-dev`.
+- For OSS: Identical to Reproducible Build steps.
 
 Invoking `make jg` using the provided makefile would run the following steps, which can also be executed manually:
 - `make fusesoc` fetches the necessary RTL using the FuseSoC tool and makes a local copy inside `build/`.
@@ -44,9 +53,15 @@ Invoking `make jg` using the provided makefile would run the following steps, wh
 - `make sv` to build the SV translation of the Sail compiler.
   Will invoke `buildspec.py`, which can be configured to adjust which instructions are defined.
   By default all of them are, this is correct but slow.
-- `jg verify.tcl` invokes Jasper interactively, sourcing the configuration & run script.
+- `jg verify.tcl` (jasper only) invokes Jasper interactively, sourcing the configuration & run script.
   Requires the above two steps to be executed first.
 
+Invoking `make build/all.aig` similarly does the following:
+- `make fusesoc`
+- `make psgen`
+- `make sv`
+- Invokes yosys (and a collection of plugins which may be found under `yosys_formal`, as well as our fork of yosys-slang) to build an Aiger file.
+
 Local versions of the external dependencies can be modified and linked into the build via Environment Variables as follows:
 - psgen: (`https://github.com/mndstrmr/psgen`)
   - Clone the repository to a local directory \<psgen-dir\> : `git clone https://github.com/mndstrmr/psgen`
@@ -66,6 +81,11 @@ Local versions of the external dependencies can be modified and linked into the
   - Make local changes...
   - In the formal-dev shell:
     - Update `LOWRISC_SAIL_RISCV_SRC` to point to the source root with `export LOWRISC_SAIL_RISCV_SRC=<sail-riscv-dir>`.
+- yosys-slang: (`https://github.com/mndstrmr/yosys-slang/tree/formal`)
+  - Clone the repository to a local directory \<yosys-slang-dir\> (`git clone https://github.com/mndstrmr/yosys-slang --branch formal`).
+  - Make local changes...
+  - In the formal-dev shell:
+    - Update `LOWRISC_YOSYS_SLANG` to point to the source root with `export LOWRISC_YOSYS_SLANG=<yosys-slang-dir>`.
 
 ## Conclusivity
 All properties are currently known to be conclusive, with the exception of M-Types.
@@ -77,9 +97,6 @@ This means:
 - We do not prove that the instruction executed with a given PC was loaded with that PC.
 - We haven't proven that Ibex resets correctly, if it doesn't there is no trace equivalence.
 
-## RTL Changes
-- `ResetAll = 1` is required for now (instead of `ResetAll = Lockstep`)
-
 ## Code Tour
 ### Top Level Goals
 The top level objective is to get proofs for `Wrap`, `Live`, `Load`, `Store` and `NoMem`.