[doc] add some content about formal in readme

readme.md

@@ -30,14 +30,15 @@ Every thing that developers want to add or modify should go into the `overlay.ni
 This skeleton provides a simple [GCD](https://en.wikipedia.org/wiki/Greatest_common_divisor) example.
 It's build script is in `nix/gcd` folder, providing the below attributes:
 
-* {gcd,tb}-compiled: JVM bytecode for the GCD/GCDTestbench and elaborator
-* {gcd,tb}-compiled.elaborator: A bash wrapper for running the elaborator with JDK
-* [tb-]elaborate: Unlowered MLIR bytecode output from firrtl elaborated by elaborator
-* [tb-]mlirbc: MLIR bytecode lowered by circt framework
-* [tb-]rtl: SystemVerilog generated from the lowered MLIR bytecode
+* {gcd,tb,formal}-compiled: JVM bytecode for the GCD/GCDTestbench and elaborator
+* {gcd,tb,formal}-compiled.elaborator: A bash wrapper for running the elaborator with JDK
+* [{tb,formal}-]elaborate: Unlowered MLIR bytecode output from firrtl elaborated by elaborator
+* [{tb,formal}-]mlirbc: MLIR bytecode lowered by circt framework
+* [{tb,formal}-]rtl: SystemVerilog generated from the lowered MLIR bytecode
 * 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
 
 To get the corresponding output, developers can use:
 
@@ -89,7 +90,17 @@ nix run '.#gcd.vcs-trace' --impure -- +dump-start=0 +dump-end=10000 +wave-path=t
 
 The DPI lib can automatically match the arguments and does not interact with VCS. In this case, the first three parameters will be passed to the DPI lib to control waveform generation, and the last parameter will be passed to the VCS to dump the results of all sva statements.
 
-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.
+* 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:
+
+```bash
+nix run '.#gcd.formal' --impure
+```
+
+and the formal verification 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.
 
 ## References