[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,43 @@
+# 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:
+  workflow_call:
+    inputs:
+      max-mem:
+        description: 'Maximum memory available for use in GB. Maximum on Pomona is ~220GB, which has ~40 min proof time. Halving memory approximately doubles proof time. '
+        required: false
+        default: '256'
+
+jobs:
+  fv:
+    name: Run the Open-Source FV flow
+    runs-on: nixos
+    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-complete --max-mem $INPUT_MAX_MEM
+

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)