[nix] add formal nix, wip

templates/chisel/nix/gcd/default.nix

@@ -58,6 +58,12 @@ in
   formal-mlirbc =
     scope.callPackage ./mlirbc.nix { elaborate = scope.formal-elaborate; };
   formal-rtl = scope.callPackage ./rtl.nix { mlirbc = scope.formal-mlirbc; };
+  formal = scope.callPackage ./formal.nix {
+    rtl = scope.formal-rtl.override {
+      enable-layers =
+        [ "Verification" "Verification.Assert" "Verification.Cover" ];
+    };
+  };
 
   # TODO: designConfig should be read from OM
   tbConfig = with builtins;

templates/chisel/nix/gcd/formal.nix

@@ -0,0 +1,4 @@
+# SPDX-License-Identifier: Apache-2.0
+# SPDX-FileCopyrightText: 2024 Jiuyang Liu <liu@jiuyang.me>
+
+{ lib, stdenv, rtl }

templates/chisel/nix/pkgs/cds-fhs-env.nix

@@ -21,7 +21,7 @@ lockedPkgs.buildFHSEnv {
   profile = ''
     [ ! -e "${jasperHome}"  ] && echo "env JASPER_HOME not set" && exit 1
     [ ! -d "${jasperHome}"  ] && echo "JASPER_HOME not accessible" && exit 1
-    [ -z "${cdsLicenseFile}"  ] && echo "env CDS LICENSE not set" && exit 1
+    [ -z "${cdsLicenseFile}"  ] && echo "env CDS_LIC_FILE not set" && exit 1
     export JASPER_HOME=${jasperHome}
     export PATH=$JASPER_HOME/bin:$PATH
     export _oldCdsEnvPath="$PATH"

templates/chisel/scripts/formal/FPV.tcl

@@ -29,13 +29,15 @@ 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
-}
+# Set exit code for ci, should only in batch mode
+
+# report -file report.txt
+# 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
+# }