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>

13 files changed, 44 insertions, 16 deletions

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/*
diff --git a/verif/formal/regfile/regfile.sby b/dv/formal/regfile/regfile.sby
index 69cb7b9..a976a29 100644
--- a/verif/formal/regfile/regfile.sby
+++ b/dv/formal/regfile/regfile.sby
@@ -1,9 +1,12 @@
 [tasks]
 cover
+bmc
 prove
 
 [options]
 cover: mode cover
+bmc: mode bmc
+bmc: depth 50
 prove: mode prove
 prove: depth 20
 
@@ -20,4 +23,4 @@ prep -top regfile_fv
 rtl/types.svh
 rtl/config_pkg.sv
 rtl/regfile.sv
-verif/formal/regfile/regfile_fv.sv
+dv/formal/regfile/regfile_fv.sv
diff --git a/verif/formal/regfile/regfile_fv.sv b/dv/formal/regfile/regfile_fv.sv
index 795024e..795024e 100644
--- a/verif/formal/regfile/regfile_fv.sv
+++ b/dv/formal/regfile/regfile_fv.sv
diff --git a/verif/formal/simple_alu/README.md b/dv/formal/simple_alu/README.md
index 3355ced..3355ced 100644
--- a/verif/formal/simple_alu/README.md
+++ b/dv/formal/simple_alu/README.md
diff --git a/verif/formal/simple_alu/simple_alu.sby b/dv/formal/simple_alu/simple_alu.sby
index cd028d9..4f4f3cd 100644
--- a/verif/formal/simple_alu/simple_alu.sby
+++ b/dv/formal/simple_alu/simple_alu.sby
@@ -17,6 +17,6 @@ read -formal -sv simple_alu_top_fv.sv
 prep -top simple_alu_top_fv
 
 [files]
-../../../rtl/simple_alu.sv
-simple_alu_fv.sv
-simple_alu_top_fv.sv
+rtl/simple_alu.sv
+dv/formal/simple_alu/simple_alu_fv.sv
+dv/formal/simple_alu/simple_alu_top_fv.sv
diff --git a/verif/formal/simple_alu/simple_alu_bind.sv b/dv/formal/simple_alu/simple_alu_bind.sv
index 8ed7057..8ed7057 100644
--- a/verif/formal/simple_alu/simple_alu_bind.sv
+++ b/dv/formal/simple_alu/simple_alu_bind.sv
diff --git a/verif/formal/simple_alu/simple_alu_fv.sv b/dv/formal/simple_alu/simple_alu_fv.sv
index 98c05a7..98c05a7 100644
--- a/verif/formal/simple_alu/simple_alu_fv.sv
+++ b/dv/formal/simple_alu/simple_alu_fv.sv
diff --git a/verif/formal/simple_alu/simple_alu_top_fv.sv b/dv/formal/simple_alu/simple_alu_top_fv.sv
index 8f1241c..8f1241c 100644
--- a/verif/formal/simple_alu/simple_alu_top_fv.sv
+++ b/dv/formal/simple_alu/simple_alu_top_fv.sv
diff --git a/tb/rv32e_model.py b/dv/tb/rv32e_model.py
index eda163e..eda163e 100644
--- a/tb/rv32e_model.py
+++ b/dv/tb/rv32e_model.py
diff --git a/tb/test.sv b/dv/tb/test.sv
index e69de29..e69de29 100644
--- a/tb/test.sv
+++ b/dv/tb/test.sv
diff --git a/verif/uvm/env.sv b/dv/uvm/env.sv
index e69de29..e69de29 100644
--- a/verif/uvm/env.sv
+++ b/dv/uvm/env.sv