[doc] rename formal to jg-fpv

chipsalliance · Sep 22, 2024 · 9a6177c · 9a6177c
1 parent 6d9dbdf
commit 9a6177c
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git 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.formal' --impure
+          nix build '.#gcd.jg-fpv' --impure
diff --git a/readme.md b/readme.md
@@ -38,7 +38,7 @@ It's build script is in `nix/gcd` folder, providing the below attributes:
 * tb-dpi-lib: DPI library written in Rust for both Verilator and VCS
 * verilated[-trace]: C++ simulation executable and libaray generated by Verilator with/without `fst` waveform trace
 * vcs[-trace]: C simulation executable compiled by VCS with/without `fsdb` waveform trace
-* formal: Formal verification report generated by JasperGold
+* jg-fpv: Formal Property Verification report generated by JasperGold
 
 To get the corresponding output, developers can use:
 
@@ -92,13 +92,13 @@ The DPI lib can automatically match the arguments and does not interact with VCS
 
 * Note that in order to use VCS for simulation, you need to set the environment variables `VC_STATIC_HOME` and `SNPSLMD_LICENSE_FILE` and add the`--impure` flag.
 
-To run the formal verification. Then you can run:
+To run the formal property verification. Then you can run:
 
 ```bash
-nix run '.#gcd.formal' --impure
+nix run '.#gcd.jg-fpv' --impure
 ```
 
-and the formal verification report will be generated in the result/
+and the report will be generated in the result/
 
 * Note that in order to use jasper gold for formal verification, you need to set the environment variables `JASPER_HOME` and `CDS_LIC_FILE` and add the`--impure` flag.
 

diff --git a/templates/chisel/nix/gcd/default.nix b/templates/chisel/nix/gcd/default.nix
@@ -60,7 +60,7 @@ in
   formal-rtl = scope.callPackage ./rtl.nix {
     mlirbc = scope.formal-mlirbc;
   };
-  formal = scope.callPackage ./formal.nix {
+  jg-fpv = scope.callPackage ./jg-fpv.nix {
     rtl = scope.formal-rtl;
   };
 

diff --git a/templates/chisel/nix/gcd/formal.nix → templates/chisel/nix/gcd/jg-fpv.nix b/templates/chisel/nix/gcd/formal.nix → templates/chisel/nix/gcd/jg-fpv.nix
@@ -7,7 +7,7 @@
 }:
 
 stdenvNoCC.mkDerivation {
-  name = "formal";
+  name = "jg-fpv";
 
   # Add "sandbox = relaxed" into /etc/nix/nix.conf, and run `systemctl restart nix-daemon`
   #