From 93a3f1b9e56c607a64c6577d8222a3cfb4c92735 Mon Sep 17 00:00:00 2001
From: drewbabel <122849144+drewbabel@users.noreply.github.com>
Date: Thu, 30 Jul 2026 17:58:41 -0700
Subject: [PATCH] [ci] Fan formal tasks out in parallel

---
 .github/workflows/ci.yml | 50 ++++++++++++++++++++++++++++++++++------
 1 file changed, 43 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b80e810..2659f71 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -25,25 +25,61 @@ jobs:
             make MOD="$mod"
           done
 
+  formal-list:
+    runs-on: ubuntu-latest
+    outputs:
+      groups: ${{ steps.list.outputs.groups }}
+    steps:
+      - uses: actions/checkout@v7
+      - name: Split formal tasks into groups
+        id: list
+        run: |
+          groups=$(python3 - <<'PY'
+          import glob, json, os, re
+          items = []
+          for f in sorted(glob.glob('formal/*.sby')):
+              mod = os.path.basename(f)[:-4]
+              block = re.search(r'^\[tasks\]\s*\n(.*?)(?=^\[|\Z)', open(f).read(), re.S | re.M)
+              tasks = [l.split()[0] for l in block.group(1).splitlines()
+                       if l.strip() and not l.lstrip().startswith('#')] if block else ['']
+              items += ['%s:%s' % (mod, t) for t in tasks]
+          g = [[] for _ in range(8)]
+          for i, x in enumerate(items):
+              g[i % 8].append(x)
+          print(json.dumps([' '.join(x) for x in g if x]))
+          PY
+          )
+          echo "$groups"
+          echo "groups=$groups" >> "$GITHUB_OUTPUT"
+
   formal:
+    needs: formal-list
     runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        group: ${{ fromJSON(needs.formal-list.outputs.groups) }}
     steps:
       - uses: actions/checkout@v7
       - uses: YosysHQ/setup-oss-cad-suite@v4
         with:
           github-token: ${{ secrets.GITHUB_TOKEN }}
-      - name: Prove every configuration
+      - name: Prove the group
         run: |
-          shopt -s nullglob
-          for sby in formal/*.sby; do
-            mod=$(basename "$sby" .sby)
-            echo "== $mod =="
-            make formal MOD="$mod"
+          for item in ${{ matrix.group }}; do
+            mod=${item%%:*}
+            task=${item#*:}
+            echo "== $mod $task =="
+            if [ -n "$task" ]; then
+              sby -f "formal/$mod.sby" "$task"
+            else
+              sby -f "formal/$mod.sby"
+            fi
           done
 
   ci-gate:
     if: always()
-    needs: [testbenches, formal]
+    needs: [testbenches, formal-list, formal]
     runs-on: ubuntu-latest
     steps:
       - name: Verify all CI jobs succeeded