Sync with 'master'feature/fu

Signed-off-by: Warrick Lo <wlo@warricklo.net>

14 files changed, 78 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/DCO b/DCO
new file mode 100644
index 0000000..49b8cb0
--- /dev/null
+++ b/DCO
@@ -0,0 +1,34 @@
+Developer Certificate of Origin
+Version 1.1
+
+Copyright (C) 2004, 2006 The Linux Foundation and its contributors.
+
+Everyone is permitted to copy and distribute verbatim copies of this
+license document, but changing it is not allowed.
+
+
+Developer's Certificate of Origin 1.1
+
+By making a contribution to this project, I certify that:
+
+(a) The contribution was created in whole or in part by me and I
+    have the right to submit it under the open source license
+    indicated in the file; or
+
+(b) The contribution is based upon previous work that, to the best
+    of my knowledge, is covered under an appropriate open source
+    license and I have the right under that license to submit that
+    work with modifications, whether created in whole or in part
+    by me, under the same open source license (unless I am
+    permitted to submit under a different license), as indicated
+    in the file; or
+
+(c) The contribution was provided directly to me by some other
+    person who certified (a), (b) or (c) and I have not modified
+    it.
+
+(d) I understand and agree that this project and the contribution
+    are public and that a record of the contribution (including all
+    personal information I submit with it, including my sign-off) is
+    maintained indefinitely and may be redistributed consistent with
+    this project or the open source license(s) involved.
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