[formal] use filelist as source

.github/workflows/main.yml

@@ -88,4 +88,4 @@ jobs:
           ref: ${{ github.event.pull_request.head.sha }}
       - name: "Run Formal Verification"
         run: |
-          nix build '.#gcd.jg-fpv' --impure
+          nix build '.#gcd.jg-fpv' --impure && $(exit $(cat result/failed_num))

templates/chisel/nix/gcd/jg-fpv.nix

@@ -43,6 +43,7 @@ stdenvNoCC.mkDerivation {
     mkdir -p $out
     
     cp report.txt $out
+    cp failed_num $out
     cp -r jgproject $out
 
     runHook postInstall

templates/chisel/nix/gcd/scripts/FPV.tcl

@@ -1,18 +1,21 @@
-# Make sure you have run the nix build command to build the formal results
-# Now the result/ directory should contain the GCD.sv and GCDFormal.sv
-
 clear -all
 
-# Analyze design under verification files
-set RESULT_PATH .
-
 # Analyze source files and property files
-analyze -sv12 \
-  ${RESULT_PATH}/GCD.sv \
-  ${RESULT_PATH}/GCDFormal.sv
+set fd [open ./filelist.f r]
+if {$fd < 0} {
+  error "File open failed!"
+}
+set filelist [split [read $fd] "\n"]
+close $fd
+
+foreach file $filelist {
+  if {[string length $file]} {
+    analyze -sv12 \ $file
+  }
+}
 
 # Elaborate design and properties
-elaborate -top GCDFormal
+elaborate
 
 # Set up Clocks and Resets
 clock clock
@@ -32,8 +35,10 @@ 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
 }
+set failed_num [open failed_num w]
+puts $failed_num "$length"
+close $failed_num
+exit 0