From 2a010dcd628d482cedd1aa7534d8e05644426cc7 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 23 Feb 2024 11:15:19 +1300 Subject: [PATCH] Add README.md and tidy source - Update .gitignores to ignore sql databases generated in new SBY. - Rename `pspin.sby` -> `pspin_test.sby` to avoid databases ending up in the source directory. - Update makefiles so that `all` target calls `clone` and `patch` targets. - Add `clone`, `patch` and `clean` targets to cv32 make. - Rename `target` task in veer to `fail`, adding `expect fail` for `fail` task and reducing bmc depth to 40. - Add `--keep-going` flag to cv32 `pdr` task. - Add `pdr_demo` task to cv32 with a timeout of 15 minutes. --- README.md | 119 ++++++++++++++++++++++++++++ cv32e40x/.gitignore | 1 + cv32e40x/Makefile | 15 +++- cv32e40x/cv32e40x.sby | 9 ++- pspin/{pspin.sby => pspin_test.sby} | 0 veer/.gitignore | 1 + veer/Makefile | 7 +- veer/veer_benchmark.sby | 9 ++- 8 files changed, 152 insertions(+), 9 deletions(-) create mode 100644 README.md rename pspin/{pspin.sby => pspin_test.sby} (100%) diff --git a/README.md b/README.md new file mode 100644 index 0000000..8007180 --- /dev/null +++ b/README.md @@ -0,0 +1,119 @@ +Advanced SBY Use by Example +=========================== + +The following three designs demonstrate advanced usage of SBY for large and +complex designs. + +cv32e40x +-------- + +This design is based on openhwgroup/cv32e40x-dv/, converting the existing +[`Jasper +script`](https://github.com/openhwgroup/cv32e40x-dv/blob/main/fv/jaspergold.tcl) +to an equivalent SBY implementation. This core contains around 250 cover +statements, and 750 assertions when run in SBY. Some adjustments were required +to remove unsupported features from the SVA (especially those that rely on UVM +support). + +Just as the Jasper script relied on environment variables defined in makefiles, +so too does the SBY script. As such, it is recommended to call `make +sby-[task]` to provide the needed variables. + +```bash +cd cv32e40x +# clone cv32e40x and verification environment +make clone +# patch source +make patch +# run SBY +make sby-bmc # bmc, pdr, or cover +``` + +Automatic multiplier detection and blackboxing is not supported in SBY and must +instead be done manually in the `[script]` section with the `cutpoint` command +from Yosys. Calling `cutpoint cv32e40x_ex_stage*_0/mul.mult_i` disconnects all +the inputs to the `riscv_mult` and connects `$anyseq` cells to all of the +outputs. + +#### Note: +It is generally recommended to include all source files in the SBY `[files]` +section and only use relative references. This ensures that any changes to the +source files do not affect tasks in progress and allows for easier debugging +since only the output folder needs to be examined. For this design, most of the +files use absolute references in a series of list files which are referenced +recursively. + +veer +---- + +This design uses the [VeeR EH1 RISC-V Core](chipsalliance/Cores-VeeR-EH1) to +demonstrate the use of tasks and tags in SBY. An SVA assertion is added which +is known to fail at step 31 of BMC. + +``` +[options] +.. +fail: expect fail +.. + +[script] +.. +# remove target assertion +~fail: chformal -assert -remove veer_wrapper/formal_setup_inst.target +.. + +[file bind.sv] +module formal_setup(); +.. + always @* begin +.. + if (!rst) + target: assert (!veer_wrapper.veer.dec.tlu.synchronous_flush_e4); +.. +endmodule + +bind veer_wrapper formal_setup formal_setup_inst(.*); +``` + +```bash +cd veer +# clone VeeR +make Cores-VeeR-EH1 +# run SBY +sby [-f] veer_benchmark.sby bmc # bmc, pdr, cover, or fail +``` + +This design also includes a dma axi interface which, by default, is not +configured and will result in failing assertions. + +With a few steps, it is possible to check AXI properties via +YosysHQ-GmbH/SVA-AXI4-FVIP: +```bash +# clone AXI verification IP +make SVA-AXI4-FVIP +# patch source +make patch +# run SBY +sby [-f] veer_benchmark.sby axi-bmc # bmc, pdr, or cover +``` + +By default, the dma axi interface is not configured and will cause failed +assertions. The `axi` tag is used to avoid this by converting the assert +properties to assume properties when the AXI FVIP is not included. + +pspin +----- + +The final design is a NoC, spcl/pspin. This design is currently only setup for +BMC, but demonstrates advanced usage of `pycode` blocks for selectively +converting asserts to assume depending on the current task. + +```bash +cd pspin +# clone pspin +make pspin +# patch source +make patch +# run SBY +sby [-f] pspin_test.sby riscv-core # riscv-core, core_region, or pulp_cluster +``` diff --git a/cv32e40x/.gitignore b/cv32e40x/.gitignore index 3a97cb2..161cdd0 100644 --- a/cv32e40x/.gitignore +++ b/cv32e40x/.gitignore @@ -1 +1,2 @@ cv32e40x_*/ +cv32e40x/ diff --git a/cv32e40x/Makefile b/cv32e40x/Makefile index 47dd6dc..33bbc6d 100644 --- a/cv32e40x/Makefile +++ b/cv32e40x/Makefile @@ -1,5 +1,8 @@ .PHONY: all -all: +all: clone patch + +.PHONY: clone +clone: core-v-verif core-v-verif/core-v-cores/cv32e40x core-v-verif: git clone https://github.com/openhwgroup/core-v-verif.git @@ -13,6 +16,10 @@ core-v-verif/core-v-cores/cv32e40x: core-v-verif cd $@ \ && git checkout b658fbe0b24da9b60d18d737c4ff4cf58b15dd8f +.PHONY: patch unpatch +patch: patch-dv patch-core +unpatch: unpatch-dv unpatch-core + .PHONY: patch-dv unpatch-dv patch-dv: cd core-v-verif/cv32e40x \ @@ -45,3 +52,9 @@ export DESIGN_RTL_DIR ?= $(CV_CORE_PKG)/rtl sby-%: sby -f cv32e40x.sby $* + +.PHONY: clean +clean: + rm -rf core-v-verif + rm -rf cv32e40x + rm -rf cv32e40x_* diff --git a/cv32e40x/cv32e40x.sby b/cv32e40x/cv32e40x.sby index 1a6c864..3089581 100644 --- a/cv32e40x/cv32e40x.sby +++ b/cv32e40x/cv32e40x.sby @@ -2,6 +2,7 @@ bmc pdr cover +pdr_demo : pdr [options] bmc: mode bmc @@ -10,6 +11,12 @@ cover: mode cover depth 40 multiclock on +# timeout for demo purposes +pdr_demo: +expect timeout +timeout 900 +-- + # fst is faster than vcd for large designs fst on vcd off @@ -18,7 +25,7 @@ vcd off [engines] # keep going to continue after failed assertions bmc: smtbmc --keep-going -pdr: abc pdr +pdr: abc --keep-going pdr cover: smtbmc # Script section adapted from cv32e40x-dv/fv/jaspergold.tcl diff --git a/pspin/pspin.sby b/pspin/pspin_test.sby similarity index 100% rename from pspin/pspin.sby rename to pspin/pspin_test.sby diff --git a/veer/.gitignore b/veer/.gitignore index b1c046b..a09d725 100644 --- a/veer/.gitignore +++ b/veer/.gitignore @@ -1 +1,2 @@ veer_benchmark_*/ +veer_benchmark/ diff --git a/veer/Makefile b/veer/Makefile index eb94e5a..442ea55 100644 --- a/veer/Makefile +++ b/veer/Makefile @@ -1,5 +1,8 @@ .PHONY: all -all: +all: clone patch + +.PHONY: clone +clone: Cores-VeeR-EH1 SVA-AXI4-FVIP Cores-VeeR-EH1: git clone https://github.com/chipsalliance/Cores-VeeR-EH1 @@ -11,8 +14,6 @@ SVA-AXI4-FVIP: CORE_PATCHES = dma_ctrl.patch -clone: Cores-VeeR-EH1 SVA-AXI4-FVIP - .PHONY: patch patch: Cores-VeeR-EH1 cd Cores-VeeR-EH1 \ diff --git a/veer/veer_benchmark.sby b/veer/veer_benchmark.sby index ff1fb41..73fab31 100644 --- a/veer/veer_benchmark.sby +++ b/veer/veer_benchmark.sby @@ -2,7 +2,7 @@ bmc pdr cover -target : bmc +fail : bmc axi axi_bmc: axi bmc axi_pdr: axi pdr @@ -12,7 +12,7 @@ axi_cover: axi cover bmc: mode bmc multiclock on -depth 50 +depth 40 -- pdr: mode prove @@ -22,9 +22,10 @@ cover: mode cover multiclock on -- +fail: expect fail [engines] -bmc: smtbmc --keep-going +bmc: smtbmc pdr: abc pdr cover: smtbmc @@ -43,7 +44,7 @@ prep -flatten ~axi: chformal -assert -assert2assume veer_wrapper/veer.dma_ctrl.assert_dma_axi_* # remove target assertion -~target: chformal -assert -remove veer_wrapper/formal_setup_inst.target +~fail: chformal -assert -remove veer_wrapper/formal_setup_inst.target tee -o ../props.txt log Cover cells: tee -a ../props.txt select t:$cover -list