From 9a6177cef4f9bb4e640c48faa86caf301c6a0eda Mon Sep 17 00:00:00 2001
From: Clo91eaf <Clo91eaf@qq.com>
Date: Sun, 22 Sep 2024 11:44:43 +0800
Subject: [PATCH] [doc] rename formal to jg-fpv

---
 .github/workflows/main.yml                          | 2 +-
 readme.md                                           | 8 ++++----
 templates/chisel/nix/gcd/default.nix                | 2 +-
 templates/chisel/nix/gcd/{formal.nix => jg-fpv.nix} | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)
 rename templates/chisel/nix/gcd/{formal.nix => jg-fpv.nix} (97%)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 6a265e1..1b31e22 100644
--- 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
index 330b225..e6f0af8 100644
--- 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
index 4d99357..2c53907 100644
--- 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 b/templates/chisel/nix/gcd/jg-fpv.nix
similarity index 97%
rename from templates/chisel/nix/gcd/formal.nix
rename to templates/chisel/nix/gcd/jg-fpv.nix
index 2fee31a..b137a1e 100644
--- a/templates/chisel/nix/gcd/formal.nix
+++ b/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`
   #