diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 1b31e22..37c7ba3 100644 --- a/.github/workflows/main.yml +++ b/.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)) diff --git a/templates/chisel/nix/gcd/jg-fpv.nix b/templates/chisel/nix/gcd/jg-fpv.nix index b137a1e..a086b86 100644 --- a/templates/chisel/nix/gcd/jg-fpv.nix +++ b/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 diff --git a/templates/chisel/nix/gcd/scripts/FPV.tcl b/templates/chisel/nix/gcd/scripts/FPV.tcl index b167b91..db5c5e2 100644 --- a/templates/chisel/nix/gcd/scripts/FPV.tcl +++ b/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