[nix] complete formal nix and ci

Signed-off-by: unlsycn <unlsycn@unlsycn.com>

.github/workflows/main.yml

@@ -86,12 +86,6 @@ jobs:
       - uses: actions/checkout@v4
         with:
           ref: ${{ github.event.pull_request.head.sha }}
-      - name: "Build formal rtl"
+      - name: "Run Formal Verification"
         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
+          nix run '.#gcd.formal --impure'

templates/chisel/.gitignore

@@ -15,5 +15,3 @@ target/
 *.fst
 *.fsdb
 *.log
-
-jgproject/

templates/chisel/nix/gcd/default.nix

@@ -57,12 +57,11 @@ in
   };
   formal-mlirbc =
     scope.callPackage ./mlirbc.nix { elaborate = scope.formal-elaborate; };
-  formal-rtl = scope.callPackage ./rtl.nix { mlirbc = scope.formal-mlirbc; };
+  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" ];
-    };
+    rtl = scope.formal-rtl;
   };
 
   # TODO: designConfig should be read from OM

templates/chisel/nix/gcd/formal.nix

@@ -1,4 +1,52 @@
 # SPDX-License-Identifier: Apache-2.0
 # SPDX-FileCopyrightText: 2024 Jiuyang Liu <liu@jiuyang.me>
 
-{ lib, stdenv, rtl }
+{ stdenvNoCC
+, rtl
+, cds-fhs-env
+}:
+
+stdenvNoCC.mkDerivation {
+  name = "formal";
+
+  # Add "sandbox = relaxed" into /etc/nix/nix.conf, and run `systemctl restart nix-daemon`
+  #
+  # run nix build with "--impure" flag to build this package without chroot
+  # require license
+  __noChroot = true;
+  dontPatchELF = true;
+
+  src = rtl;
+
+  passthru = {
+    inherit rtl;
+  };
+
+  shellHook = ''
+    echo "[nix] entering fhs env"
+    ${cds-fhs-env}/bin/cds-fhs-env
+  '';
+
+  buildPhase = ''
+    runHook preBuild
+
+    echo "[nix] running Jasper"
+    fhsBash=${cds-fhs-env}/bin/cds-fhs-env
+    "$fhsBash" -c "jg -batch ${./scripts/FPV.tcl}"
+    
+    runHook postBuild
+  '';
+
+  installPhase = ''
+    runHook preInstall
+    
+    ls -l
+    mkdir -p $out
+    
+    cp report.txt $out
+    cp -r jgproject $out
+
+    runHook postInstall
+  '';
+
+}

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

@@ -4,7 +4,7 @@
 clear -all
 
 # Analyze design under verification files
-set RESULT_PATH ./result
+set RESULT_PATH .
 
 # Analyze source files and property files
 analyze -sv12 \
@@ -26,18 +26,14 @@ get_design_info
 set_max_trace_length 100
 prove -all
 
-# Report proof results
-report
-
-# 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
-# }
+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
+}

templates/chisel/nix/gcd/vcs.nix

@@ -79,7 +79,7 @@ stdenv.mkDerivation (finalAttr: {
     cp ${binName} $out/lib
     cp -r ${binName}.daidir $out/lib
 
-    substitute ${./vcs-wrapper.sh} $out/bin/${binName} \
+    substitute ${./scripts/vcs-wrapper.sh} $out/bin/${binName} \
       --subst-var-by shell "${bash}/bin/bash" \
       --subst-var-by dateBin "$(command -v date)" \
       --subst-var-by vcsSimBin "$out/lib/${binName}" \

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

@@ -23,6 +23,7 @@ lockedPkgs.buildFHSEnv {
     [ ! -d "${jasperHome}"  ] && echo "JASPER_HOME not accessible" && exit 1
     [ -z "${cdsLicenseFile}"  ] && echo "env CDS_LIC_FILE not set" && exit 1
     export JASPER_HOME=${jasperHome}
+    export CDS_LIC_FILE=${cdsLicenseFile}
     export PATH=$JASPER_HOME/bin:$PATH
     export _oldCdsEnvPath="$PATH"
     preHook() {