[ci] add formal ci

Author: Clo91eaf

.github/workflows/main.yml

@@ -73,3 +73,25 @@ jobs:
       - name: "Run verilator"
         run: |
           nix run '.#gcd.verilated'
+
+  run-formal-verification:
+    name: "Run Formal Verification"
+    strategy:
+      fail-fast: false
+    runs-on: [self-hosted, linux, nixos]
+    defaults:
+      run:
+        working-directory: ./templates/chisel
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
+      - name: "Build formal rtl"
+        run: |
+          nix run '.#gcd.formal-rtl'
+      - name: "Build formal environment"
+        run: |
+          nix run '.#cds-fhs-env' --impure
+      - name: "Run formal verification"
+        run: |
+          jg -batch ./scripts/formal/FPV.tcl

templates/chisel/scripts/formal/FPV.tcl

@@ -29,3 +29,13 @@ prove -all
 # Report proof results
 report
 
+# Set exit code for ci
+set failed_properties [get_property_list -include {status {cex unreachable}}]
+set length [llength $failed_properties]
+if { $length > 0 } {
+  puts "There are $length failed properties!"
+  exit 1
+} else {
+  puts "All properties passed!"
+  exit 0
+}