From 44b2587a205e483dcb9e2fa7c171458d8c160892 Mon Sep 17 00:00:00 2001 From: Clo91eaf Date: Sun, 22 Sep 2024 00:52:13 +0800 Subject: [PATCH] [doc] add some content about formal in readme --- readme.md | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/readme.md b/readme.md index c1654ce..330b225 100644 --- a/readme.md +++ b/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