From d0b54f12d84dd0d9bc6e48e1e24b137032055dc3 Mon Sep 17 00:00:00 2001 From: unlsycn Date: Sat, 21 Sep 2024 17:24:57 +0000 Subject: [PATCH] [nix] complete formal nix and ci Signed-off-by: unlsycn --- .github/workflows/main.yml | 10 +--- templates/chisel/.gitignore | 2 - templates/chisel/nix/gcd/default.nix | 9 ++-- templates/chisel/nix/gcd/formal.nix | 50 ++++++++++++++++++- .../formal => nix/gcd/scripts}/FPV.tcl | 28 +++++------ .../nix/gcd/{ => scripts}/vcs-wrapper.sh | 0 templates/chisel/nix/gcd/vcs.nix | 2 +- templates/chisel/nix/pkgs/cds-fhs-env.nix | 1 + 8 files changed, 69 insertions(+), 33 deletions(-) rename templates/chisel/{scripts/formal => nix/gcd/scripts}/FPV.tcl (61%) rename templates/chisel/nix/gcd/{ => scripts}/vcs-wrapper.sh (100%) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 7db413f..529792a 100644 --- a/.github/workflows/main.yml +++ b/.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' diff --git a/templates/chisel/.gitignore b/templates/chisel/.gitignore index 6a0f020..338f9fc 100644 --- a/templates/chisel/.gitignore +++ b/templates/chisel/.gitignore @@ -15,5 +15,3 @@ target/ *.fst *.fsdb *.log - -jgproject/ \ No newline at end of file diff --git a/templates/chisel/nix/gcd/default.nix b/templates/chisel/nix/gcd/default.nix index 5a3a2cb..4d99357 100644 --- a/templates/chisel/nix/gcd/default.nix +++ b/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 diff --git a/templates/chisel/nix/gcd/formal.nix b/templates/chisel/nix/gcd/formal.nix index 1372289..9f5a7d0 100644 --- a/templates/chisel/nix/gcd/formal.nix +++ b/templates/chisel/nix/gcd/formal.nix @@ -1,4 +1,52 @@ # SPDX-License-Identifier: Apache-2.0 # SPDX-FileCopyrightText: 2024 Jiuyang Liu -{ lib, stdenv, rtl } \ No newline at end of file +{ 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 + ''; + +} diff --git a/templates/chisel/scripts/formal/FPV.tcl b/templates/chisel/nix/gcd/scripts/FPV.tcl similarity index 61% rename from templates/chisel/scripts/formal/FPV.tcl rename to templates/chisel/nix/gcd/scripts/FPV.tcl index 26e56ec..b167b91 100644 --- a/templates/chisel/scripts/formal/FPV.tcl +++ b/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 -# } \ No newline at end of file +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 +} diff --git a/templates/chisel/nix/gcd/vcs-wrapper.sh b/templates/chisel/nix/gcd/scripts/vcs-wrapper.sh similarity index 100% rename from templates/chisel/nix/gcd/vcs-wrapper.sh rename to templates/chisel/nix/gcd/scripts/vcs-wrapper.sh diff --git a/templates/chisel/nix/gcd/vcs.nix b/templates/chisel/nix/gcd/vcs.nix index 40bb5c2..f951da4 100644 --- a/templates/chisel/nix/gcd/vcs.nix +++ b/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}" \ diff --git a/templates/chisel/nix/pkgs/cds-fhs-env.nix b/templates/chisel/nix/pkgs/cds-fhs-env.nix index f34dab8..af95332 100644 --- a/templates/chisel/nix/pkgs/cds-fhs-env.nix +++ b/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() {