Introduce an OSS Formal Flow

.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

.github/workflows/ci-formal.yml

@@ -0,0 +1,48 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# GitHub Actions CI build configuration
+
+name: Ibex OSS Formal CI
+
+on:
+  pull_request:
+    branches:
+      - '*'
+
+jobs:
+  fv:
+    name: Run the Open-Source FV flow
+    runs-on: nixos
+    concurrency:
+      group: oss-fv
+      cancel-in-progress: false # Only do one oss-fv job at a time, since we will use a huge amount of memory
+    steps:
+      - name: Setup env
+        run: |
+          echo "MAX_MEM_GB=100" >> $GITHUB_ENV # Maximum memory available to conductor.py, which is inversely proportional to time. 200GB -> 40 mins
+          echo "NIX_CONFIG=accept-flake-config = true" >> $GITHUB_ENV
+
+      - name: Notify about queued execution
+        run: |
+          echo "Warning: This job will block other oss-fv jobs until it finishes, since it uses a lot of memory."
+
+      - uses: actions/checkout@v4
+
+      - name: Install Nix
+        uses: cachix/install-nix-action@v27
+        with:
+          extra_nix_config: |
+            substituters = https://nix-cache.lowrisc.org/public/ https://cache.nixos.org/
+            trusted-public-keys = nix-cache.lowrisc.org-public-1:O6JLD0yXzaJDPiQW1meVu32JIDViuaPtGDfjlOopU7o= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
+
+      - name: Run OSS Env
+        run: |
+          source <(nix print-dev-env .#oss-dev)
+
+          cd dv/formal
+          make build/aig-manip
+          make build/all.aig SHELL=bash
+          python3 conductor.py prove --check-complete --max-mem $MAX_MEM_GB
+

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,29 +1,42 @@
+# 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
 
-include Sources.mk
+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
 
-SAIL_SV_FLAGS=-sv -sv-comb -sv-inregs -sv-outregs -sv-nostrings -sv-nopacked -sv-nomem -Oconstant_fold -memo-z3 \
-	-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 2:rX \
+# -sv, use the SystemVerilog backend
+# --sv-comb, generate a always_comb instead of an initial block
+# --sv-inregs --sv-outregs, produce inputs and outputs for every Sail register
+# --sv-nostrings, --sv-nopacked, --sv-nomem, avoid generating some things Jasper doesn't like (FIXME: --sv-nopacked might be better removed?)
+# -Oconstrant_fold, do basic optimisation
+# -memo-z3, resolving types requires a sat solver, this helps speed up those queries
+# --sv-unreachable, remove the implementations of functions to either make the design smaller or avoid recursion loops (FIXME: Still necessary?)
+# --sv-fun2wires (n:)?f, transform a function into ports, with n (or 1) slots
+SAIL_SV_FLAGS=-sv --sv-comb --sv-inregs --sv-outregs --sv-nostrings --sv-nopacked --sv-nomem -Oconstant_fold -memo-z3 \
+	--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
 
 # 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) \
@@ -32,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`.