From adce21a91f4b55cad1126fa4d453b4d6eef79f7f Mon Sep 17 00:00:00 2001
From: Warrick Lo <wlo@warricklo.net>
Date: Wed, 24 Jun 2026 07:58:06 +0000
Subject: Add CI pipeline for formal verification

* Add formal verification tests with sby to CI
* Fix reviewdog having insufficient API permissions

See-also: #15
Signed-off-by: Warrick Lo <wlo@warricklo.net>
---
 .github/workflows/format.yaml | 11 +++++++----
 .github/workflows/lint.yaml   | 16 ++++++++--------
 .github/workflows/test.yaml   | 22 ++++++++++++++++++++++
 3 files changed, 37 insertions(+), 12 deletions(-)
 create mode 100644 .github/workflows/test.yaml

(limited to '.github/workflows')

diff --git a/.github/workflows/format.yaml b/.github/workflows/format.yaml
index fbef4a8..1c32511 100644
--- a/.github/workflows/format.yaml
+++ b/.github/workflows/format.yaml
@@ -5,8 +5,11 @@ on: [pull_request]
 jobs:
   format:
     runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      pull-requests: write
     steps:
-      - uses: actions/checkout@master
-      - uses: chipsalliance/verible-formatter-action@main
-        with:
-          github_token: ${{ secrets.GITHUB_TOKEN }}
+    - uses: actions/checkout@master
+    - uses: chipsalliance/verible-formatter-action@main
+      with:
+        github_token: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.github/workflows/lint.yaml b/.github/workflows/lint.yaml
index 94ad728..91424ca 100644
--- a/.github/workflows/lint.yaml
+++ b/.github/workflows/lint.yaml
@@ -6,11 +6,11 @@ jobs:
   lint:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@master
-      - uses: chipsalliance/verible-linter-action@main
-        with:
-          config_file: "lint.rules"
-          github_token: ${{ secrets.GITHUB_TOKEN }}
-      - name: Fail on lint errors
-        run: |
-          verible-verilog-lint --lint_fatal=true --rules_config=lint.rules $(find . -name "*.sv" -o -name "*.v")
+    - uses: actions/checkout@master
+    - uses: chipsalliance/verible-linter-action@main
+      with:
+        config_file: "lint.rules"
+        github_token: ${{ secrets.GITHUB_TOKEN }}
+    - name: Fail on lint errors
+      run: |
+        verible-verilog-lint --lint_fatal=true --rules_config=lint.rules $(find . -name "*.sv" -o -name "*.v")
diff --git a/.github/workflows/test.yaml b/.github/workflows/test.yaml
new file mode 100644
index 0000000..ee45561
--- /dev/null
+++ b/.github/workflows/test.yaml
@@ -0,0 +1,22 @@
+name: Test
+
+on: [push, pull_request]
+
+jobs:
+  formal:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@master
+    - uses: YosysHQ/setup-oss-cad-suite@v4
+    - name: Run test
+      shell: bash
+      run: |
+        sby -f dv/formal/regfile/regfile.sby
+    - name: Upload artifacts
+      uses: actions/upload-artifact@v7
+      with:
+        name: formal-verification
+        path: |
+          dv/formal/regfile/regfile_bmc/*
+          dv/formal/regfile/regfile_cover/*
+          dv/formal/regfile/regfile_prove/*
-- 
cgit v1.2.3