Skip to content

Commit 961a625

Browse files
committed
[doc] rename formal to jg-fpv
1 parent 6d9dbdf commit 961a625

File tree

4 files changed

+7
-7
lines changed

4 files changed

+7
-7
lines changed

.github/workflows/main.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,4 +88,4 @@ jobs:
8888
ref: ${{ github.event.pull_request.head.sha }}
8989
- name: "Run Formal Verification"
9090
run: |
91-
nix build '.#gcd.formal' --impure
91+
nix build '.#gcd.jg-fpv' --impure

readme.md

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ It's build script is in `nix/gcd` folder, providing the below attributes:
3838
* tb-dpi-lib: DPI library written in Rust for both Verilator and VCS
3939
* verilated[-trace]: C++ simulation executable and libaray generated by Verilator with/without `fst` waveform trace
4040
* vcs[-trace]: C simulation executable compiled by VCS with/without `fsdb` waveform trace
41-
* formal: Formal verification report generated by JasperGold
41+
* jg-fpv: Formal Property Verification report generated by JasperGold
4242

4343
To get the corresponding output, developers can use:
4444

@@ -92,13 +92,13 @@ The DPI lib can automatically match the arguments and does not interact with VCS
9292

9393
* 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.
9494

95-
To run the formal verification. Then you can run:
95+
To run the formal property verification. Then you can run:
9696

9797
```bash
98-
nix run '.#gcd.formal' --impure
98+
nix build '.#gcd.jg-fpv' --impure
9999
```
100100

101-
and the formal verification report will be generated in the result/
101+
and the report will be generated in the result/
102102

103103
* 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.
104104

templates/chisel/nix/gcd/default.nix

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ in
6060
formal-rtl = scope.callPackage ./rtl.nix {
6161
mlirbc = scope.formal-mlirbc;
6262
};
63-
formal = scope.callPackage ./formal.nix {
63+
jg-fpv = scope.callPackage ./jg-fpv.nix {
6464
rtl = scope.formal-rtl;
6565
};
6666

templates/chisel/nix/gcd/formal.nix renamed to templates/chisel/nix/gcd/jg-fpv.nix

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
}:
88

99
stdenvNoCC.mkDerivation {
10-
name = "formal";
10+
name = "jg-fpv";
1111

1212
# Add "sandbox = relaxed" into /etc/nix/nix.conf, and run `systemctl restart nix-daemon`
1313
#

0 commit comments

Comments
 (0)