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

@@ -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
+```

cv32e40x/.gitignore

@@ -1 +1,2 @@
 cv32e40x_*/
+cv32e40x/

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_*

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

veer/.gitignore

@@ -1 +1,2 @@
 veer_benchmark_*/
+veer_benchmark/

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 \

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