Use the test Makefile for all examples

* Rename and move sbysrc/demo[123].sby to docs/examples/demos
    * Make them use multiple tasks for multiple engines
* Scan docs/examples for sby files for make test
* `make ci` is now `NOSKIP` by default
* Skip scripts using `verific` w/o yosys verific support
    * This does not fail even with NOSKIP set

.github/workflows/ci.yml

@@ -9,4 +9,4 @@ jobs:
       - uses: actions/checkout@v2
       - uses: YosysHQ/setup-oss-cad-suite@v1
       - name: Run checks
-        run: tabbypip install xmlschema && make ci NOSKIP=1
+        run: tabbypip install xmlschema && make ci

Makefile

@@ -21,10 +21,10 @@ help:
 	@echo "    build documentation in docs/build/html/"
 	@echo ""
 	@echo "make test"
-	@echo "    run tests"
+	@echo "    run tests, skipping tests with missing dependencies"
 	@echo ""
 	@echo "make ci"
-	@echo "    run tests and check examples"
+	@echo "    run all tests, failing tests with missing dependencies"
 	@echo "    note: this requires a full Tabby CAD Suite or OSS CAD Suite install"
 	@echo ""
 	@echo "make clean"
@@ -50,15 +50,8 @@ endif
 ci: check_cad_suite
 	@$(MAKE) run_ci
 
-run_ci: \
-  test_demo1 test_demo2 test_demo3 \
-  test_abstract_abstr test_abstract_props \
-  test_demos_fib_cover test_demos_fib_prove test_demos_fib_live \
-  test_multiclk_dpmem \
-  test_puzzles_djb2hash test_puzzles_pour853to4 test_puzzles_wolfgoatcabbage \
-  test_puzzles_primegen_primegen test_puzzles_primegen_primes_pass test_puzzles_primegen_primes_fail \
-  test_quickstart_demo test_quickstart_cover test_quickstart_prove test_quickstart_memory \
-  test
+run_ci:
+	$(MAKE) test NOSKIP=1
 	if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
 		YOSYS_NOVERIFIC=1 $(MAKE) run_ci; \
 	fi
@@ -79,58 +72,6 @@ test_demo2:
 test_demo3:
 	cd sbysrc && python3 sby.py -f demo3.sby
 
-test_abstract_abstr:
-	@if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
-		cd docs/examples/abstract && python3 ../../../sbysrc/sby.py -f abstr.sby; \
-	else echo "skipping $@"; fi
-
-test_abstract_props:
-	if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
-		cd docs/examples/abstract && python3 ../../../sbysrc/sby.py -f props.sby; \
-	else echo "skipping $@"; fi
-
-test_demos_fib_cover:
-	cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby cover
-
-test_demos_fib_prove:
-	cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby prove
-
-test_demos_fib_live:
-	cd docs/examples/demos && python3 ../../../sbysrc/sby.py -f fib.sby live
-
-test_multiclk_dpmem:
-	cd docs/examples/multiclk && python3 ../../../sbysrc/sby.py -f dpmem.sby
-
-test_puzzles_djb2hash:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f djb2hash.sby
-
-test_puzzles_pour853to4:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f pour_853_to_4.sby
-
-test_puzzles_wolfgoatcabbage:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f wolf_goat_cabbage.sby
-
-test_puzzles_primegen_primegen:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primegen
-
-test_puzzles_primegen_primes_pass:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primes_pass
-
-test_puzzles_primegen_primes_fail:
-	cd docs/examples/puzzles && python3 ../../../sbysrc/sby.py -f primegen.sby primes_fail
-
-test_quickstart_demo:
-	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f demo.sby
-
-test_quickstart_cover:
-	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f cover.sby
-
-test_quickstart_prove:
-	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f prove.sby
-
-test_quickstart_memory:
-	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f memory.sby
-
 test:
 	$(MAKE) -C tests test
 

docs/examples/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples
+TESTDIR=../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/abstract/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples/abstract
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/demos/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples/demos
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/demos/picorv32_axicheck.sby

@@ -0,0 +1,25 @@
+[tasks]
+yices
+boolector
+z3
+abc
+
+[options]
+mode bmc
+depth 10
+
+[engines]
+yices: smtbmc yices
+boolector: smtbmc boolector -ack
+z3: smtbmc --nomem z3
+abc: abc bmc3
+
+[script]
+read_verilog -formal -norestrict -assume-asserts picorv32.v
+read_verilog -formal axicheck.v
+prep -top testbench
+
+[files]
+picorv32.v ../../../extern/picorv32.v
+axicheck.v ../../../extern/axicheck.v
+

docs/examples/demos/up_down_counter.sby

@@ -1,10 +1,13 @@
+[tasks]
+suprove
+avy
+
 [options]
 mode prove
-wait on
 
 [engines]
-aiger suprove
-aiger avy
+suprove: aiger suprove
+avy: aiger avy
 
 [script]
 read_verilog -formal demo.v

docs/examples/indinv/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples/indinv
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/multiclk/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples/multiclk
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/puzzles/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples/puzzles
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk

docs/examples/quickstart/Makefile

@@ -0,0 +1,3 @@
+SUBDIR=../docs/examples/quickstart
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk

sbysrc/demo1.sby

@@ -1,21 +0,0 @@
-
-[options]
-mode bmc
-depth 10
-wait on
-
-[engines]
-smtbmc yices
-smtbmc boolector -ack
-smtbmc --nomem z3
-abc bmc3
-
-[script]
-read_verilog -formal -norestrict -assume-asserts picorv32.v
-read_verilog -formal axicheck.v
-prep -top testbench
-
-[files]
-picorv32.v ../extern/picorv32.v
-axicheck.v ../extern/axicheck.v
-

sbysrc/sby.py

@@ -381,6 +381,7 @@ if dump_taskinfo:
         taskinfo[taskname or ""] = {
             "mode": cfg.options.get("mode"),
             "engines": cfg.engines,
+            "script": cfg.script,
         }
     print(json.dumps(taskinfo, indent=2))
     sys.exit(0)

tests/make/collect_tests.py

@@ -26,6 +26,7 @@ def collect(path):
 
 
 collect(Path("."))
+collect(Path("../docs/examples"))
 
 out_file = Path("make/rules/collect.mk")
 out_file.parent.mkdir(exist_ok=True)

tests/make/required_tools.py

@@ -36,6 +36,15 @@ if __name__ == "__main__":
         with open("make/rules/found_tools") as found_tools_file:
             found_tools = set(tool.strip() for tool in found_tools_file.readlines())
 
+        if 'verific' in required_tools:
+            result = subprocess.run(["yosys", "-qp", "read -verific"], capture_output=True)
+            if result.returncode:
+                print()
+                print(f"SKIPPING {target}: requires yosys with verific support")
+                print()
+                exit()
+            required_tools.remove('verific')
+
         missing_tools = sorted(
             f"`{tool}`" for tool in required_tools if tool not in found_tools
         )

tests/make/subdir.mk

@@ -1,15 +1,17 @@
+TESTDIR ?= ..
+
 test:
-	@$(MAKE) -C .. $(SUBDIR)/$@
+	@$(MAKE) -C $(TESTDIR) $(SUBDIR)/$@
 
 .PHONY: test refresh IMPLICIT_PHONY
 
 IMPLICIT_PHONY:
 
 refresh:
-	@$(MAKE) -C .. refresh
+	@$(MAKE) -C $(TESTDIR) refresh
 
 help:
-	@$(MAKE) -C .. help
+	@$(MAKE) -C $(TESTDIR) help
 
 %: IMPLICIT_PHONY
-	@$(MAKE) -C .. $(SUBDIR)/$@
+	@$(MAKE) -C $(TESTDIR) $(SUBDIR)/$@

tests/make/test_rules.py

@@ -56,6 +56,9 @@ with rules_file.open("w") as rules:
                 solvers.add(solver)
                 engine_solvers.add((engine, solver))
 
+        if any(line.startswith("read -verific") or line.startswith("verific") for line in info["script"]):
+            required_tools.add("verific")
+
         required_tools = sorted(required_tools)
 
         print(f".PHONY: {target}", file=rules)