[ci] Add OSS-formal CI

Adds an OSS-Formal CI pass running on ponoma, it takes ~1hr 9mins to run
at this time, which is quite fast!

Author: mndstrmr

.github/workflows/ci-formal.yml

@@ -0,0 +1,56 @@
+# 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:
+  push:
+    paths:
+      - 'flake.nix'
+      - 'flake.lock'
+      - 'dv/formal/**'
+      - 'rtl/**'
+      - 'vendor/**'
+      - '.github/**'
+  merge_group:
+    types:
+      - checks_requested
+  pull_request:
+    paths:
+      - 'flake.nix'
+      - 'flake.lock'
+      - 'dv/formal/**'
+      - 'rtl/**'
+      - 'vendor/**'
+      - '.github/**'
+
+jobs:
+  fv:
+    name: Run the Open-Source FV flow
+    runs-on: nixos-25.05
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Setup env
+        run: |
+          echo "NIX_CONFIG=accept-flake-config = true" >> $GITHUB_ENV
+
+      - 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-all
+

dv/formal/Makefile

@@ -33,7 +33,7 @@ build/fusesoc: $(IBEX_ROOT)/rtl $(IBEX_ROOT)/vendor
 	  lowrisc:ibex:ibex_formal:0.1
 	touch build/fusesoc # Fix timestamps for Makefile
 
-build/ibexspec.sv: $(SAIL) $(SAIL_SRCS) $(SAIL_EXTRA_SRCS) Sources.mk Makefile spec/fix_bugs.py
+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
@@ -53,6 +53,7 @@ build/yosys_formal.so: yosys_formal/global_clock.cc yosys_formal/write_aiger.cc
 	yosys-config --build build/yosys_formal.so yosys_formal/global_clock.cc yosys_formal/write_aiger.cc yosys_formal/opt_muxtree.cc
 
 build/aig-manip: aig-manip/src/main.rs
+	mkdir -p build
 	cd aig-manip && cargo build --release
 	cp aig-manip/target/release/aig-manip build/
 

dv/formal/check/top.sv

@@ -1,5 +1,5 @@
 // Copyright lowRISC contributors.
-// Copyright 2024 University of Oxford, see also CREDITS.md.
+// Copyright 2025 University of Oxford, see also CREDITS.md.
 // Licensed under the Apache License, Version 2.0, see LICENSE for details.
 // Original author: Louis-Emile Ploix
 // SPDX-License-Identifier: Apache-2.0

dv/formal/conductor.py

@@ -448,6 +448,7 @@ def group(props):
 parser.add_argument("--hard", action="store_true", help="In explore mode, try harder to prove properties (1hr timeout, more engines).")
 parser.add_argument("--no-run", action="store_true", help="In explore mode don't run proofs again to check steps.")
 parser.add_argument("--no-kill", action="store_true", help="Don't kill proof processes due to running out of memory.")
+parser.add_argument("--check-complete", action="store_true", help="In prove mode, fail if there are unskipped properties without proofs.")
 args = parser.parse_args()
 
 SKIPPED_PROPS = [
@@ -535,7 +536,7 @@ async def info_mode(by_step, by_step_skipped):
             print(red(f"Step {step} :: UNACCOUNTED :: :: :: {' '.join(unaccounted)}"))
     print(f"{total_steps} proof steps in total")
 
-async def prove_mode(by_step):
+async def prove_mode(all_props, by_step):
     all_strategies = []
     for step, props in enumerate(by_step):
         if step < args.start:
@@ -555,6 +556,17 @@ async def prove_mode(by_step):
         else:
             all_strategies.extend(strategy)
 
+    if args.check_complete:
+        covered = set()
+        for step in all_strategies:
+            covered.update(step[1])
+        uncovered = set(prop[1] for prop in all_props).difference(covered)
+        if len(uncovered) > 0:
+            print(red(f"Missing proof steps for {len(uncovered)} properties: {' '.join(uncovered)}"))
+            exit(1)
+        else:
+            print(green(f"All {len(all_props)} properties are covered."))
+
     if not args.by_step:
         print(white(f"Running strategy for everything"))
         run_start = time.time()
@@ -563,12 +575,16 @@ async def prove_mode(by_step):
         print(white(f"Ran strategy in {run_dt:.3f}s"))
 
         unsats = 0
+        has_errors = False
         for res, step in results:
             if res[0] == 20:
                 unsats += 1
             else:
+                has_errors = True
                 print(red(f"Failed to prove step {step[0]} proof step with code {res[0]} (see above, or logfile.txt, for more details): {' '.join(step[1])}"))
-        print(white(f"{unsats}/{len(all_strategies)} proofs steps were UNSAT"))
+        print(white(f"{unsats}/{len(all_strategies)} proof steps were UNSAT"))
+        if has_errors:
+            exit(1) # Failed
 
 async def construct_strategy(step, props):
     strategy = load_strategy(step) or []
@@ -658,7 +674,6 @@ async def logopt(by_step):
             continue
         [props, step, sha, config] = ins
         if len(outs) != 6 or type(outs[0]) != int or type(outs[1]) != float or type(outs[2]) != float or type(outs[3]) != str or type(outs[4]) != str or type(outs[4]) != str:
-            print("ERR 2")
             continue
         [code, mem, dt, kind, stdout, stderr] = outs
         props.sort()
@@ -740,7 +755,7 @@ def group_by_step(names, max=None):
         case "info":
             await info_mode(by_step, skipped_by_step)
         case "prove":
-            await prove_mode(by_step)
+            await prove_mode(props, by_step)
         case "explore":
             await explore_mode(by_step)
         case "logopt":

flake.nix

@@ -206,7 +206,7 @@
             oss-dev = mkshell-minimal {
               packages = standard_deps ++ [
                 lowrisc_yosys_slang
-                (pkgs.yosys.override (attrs: { enablePython = false; }))
+                ((pkgs.yosys.override (attrs: { enablePython = false; })).overrideAttrs (finalAttrs: prev: { doCheck = false; }))
               ] ++ (with pkgs; [
                 gtkwave # not stricly necesssary
                 ric3