[ci] Have an OSS-Formal CI Pass

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.

An input (max-mem) is provided to limit memory usage.

Author: mndstrmr

.github/workflows/ci-formal.yml

@@ -0,0 +1,47 @@
+# 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: 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: 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-complete
+

dv/formal/conductor.py

@@ -225,13 +225,13 @@ class ProcessRunner:
     MAX_RUNNING = (psutil.cpu_count() or 8) - 2 # Number of CPUs, with a couple spares
 
     def __init__(self):
-        log(f"Process runner will have a maximum of {ProcessRunner.MAX_RUNNING} processes, and currently sees {global_memory_free():.3f}GB free.")
-
         self.pending = []
         self.running = []
         self.first_start = time.time()
         self.debug_count = 0
 
+        log(f"Process runner will have a maximum of {ProcessRunner.MAX_RUNNING} processes, and currently sees {self.mem_avail():.3f}GB free.")
+
     def append(self, proc):
         self.pending.insert(0, proc)
 
@@ -244,7 +244,7 @@ def children_used_mem(self):
     def mem_avail(self):
         if args.max_mem == 0:
             return global_memory_free()
-        return max(args.max_mem - self.children_used_mem(), 0)
+        return min(global_memory_free(), max(args.max_mem - self.children_used_mem(), 0))
 
     def poll(self):
         # Kill recently started processes until memory is OK, unless there is just one, then there's no point(?)
@@ -279,9 +279,10 @@ def poll(self):
 
         asyncio.get_running_loop().call_later(ProcessRunner.POLL_DELAY, lambda: self.poll())
 
-process_runner = ProcessRunner()
+process_runner: ProcessRunner | None = None
 '''Run a shell command in the global process runner'''
 async def shell(cmd, expected_memory = 0.0, timeout = None, debug_slow = None):
+    assert process_runner is not None
     proc = Process(cmd, expected_memory=expected_memory, timeout=timeout, debug_slow=debug_slow)
     process_runner.append(proc)
     return await proc.future
@@ -720,6 +721,8 @@ async def explore_mode(by_step: list[list[str]]):
             log(f"Skipping proof run for step {step}, since it has just one step", c=white)
 
 async def main():
+    global process_runner
+
     def preproc_name(name: str) -> tuple[int, str]:
         first = name.split("$")[1][5:]
         assert first.startswith("Step")
@@ -738,6 +741,7 @@ def group_by_step(names: list[tuple[int, str]], max=None) -> list[list[str]]:
                 by_step.append([])
         return by_step
 
+    process_runner = ProcessRunner()
     process_runner.start_loop()
 
     log("Reading property list", c=white)