From a89afdec96aa17b84b3de3dd5b0c92989487fbb9 Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Sat, 21 Sep 2024 22:50:33 +0800
Subject: [PATCH] [nix] add formal nix, wip

---
 templates/chisel/nix/gcd/default.nix      |  6 ++++++
 templates/chisel/nix/gcd/formal.nix       |  4 ++++
 templates/chisel/nix/pkgs/cds-fhs-env.nix |  2 +-
 templates/chisel/scripts/formal/FPV.tcl   | 22 ++++++++++++----------
 4 files changed, 23 insertions(+), 11 deletions(-)
 create mode 100644 templates/chisel/nix/gcd/formal.nix

diff --git a/templates/chisel/nix/gcd/default.nix b/templates/chisel/nix/gcd/default.nix
index dfb1c79..5a3a2cb 100644
--- a/templates/chisel/nix/gcd/default.nix
+++ b/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;
diff --git a/templates/chisel/nix/gcd/formal.nix b/templates/chisel/nix/gcd/formal.nix
new file mode 100644
index 0000000..1372289
--- /dev/null
+++ b/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 }
\ No newline at end of file
diff --git a/templates/chisel/nix/pkgs/cds-fhs-env.nix b/templates/chisel/nix/pkgs/cds-fhs-env.nix
index c6e527a..f34dab8 100644
--- a/templates/chisel/nix/pkgs/cds-fhs-env.nix
+++ b/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"
diff --git a/templates/chisel/scripts/formal/FPV.tcl b/templates/chisel/scripts/formal/FPV.tcl
index 1280b48..26e56ec 100644
--- a/templates/chisel/scripts/formal/FPV.tcl
+++ b/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
-}
\ No newline at end of file
+# 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
+# }
\ No newline at end of file