From 499371fd39075915fe1a4ac83164e4e426c40d78 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 13 Jun 2022 13:20:33 +0200 Subject: [PATCH] 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 | 2 +- Makefile | 67 ++----------------- docs/examples/Makefile | 3 + docs/examples/abstract/Makefile | 3 + docs/examples/demos/Makefile | 3 + .../examples/demos/memory.sby | 0 docs/examples/demos/picorv32_axicheck.sby | 25 +++++++ .../examples/demos/up_down_counter.sby | 9 ++- docs/examples/indinv/Makefile | 3 + docs/examples/multiclk/Makefile | 3 + docs/examples/puzzles/Makefile | 3 + docs/examples/quickstart/Makefile | 3 + sbysrc/demo1.sby | 21 ------ sbysrc/sby.py | 1 + tests/make/collect_tests.py | 1 + tests/make/required_tools.py | 9 +++ tests/make/subdir.mk | 10 +-- tests/make/test_rules.py | 3 + 18 files changed, 77 insertions(+), 92 deletions(-) create mode 100644 docs/examples/Makefile create mode 100644 docs/examples/abstract/Makefile create mode 100644 docs/examples/demos/Makefile rename sbysrc/demo3.sby => docs/examples/demos/memory.sby (100%) create mode 100644 docs/examples/demos/picorv32_axicheck.sby rename sbysrc/demo2.sby => docs/examples/demos/up_down_counter.sby (85%) create mode 100644 docs/examples/indinv/Makefile create mode 100644 docs/examples/multiclk/Makefile create mode 100644 docs/examples/puzzles/Makefile create mode 100644 docs/examples/quickstart/Makefile delete mode 100644 sbysrc/demo1.sby diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 67abe1f..ea48d06 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/Makefile b/Makefile index 07f85a4..7a86f6b 100644 --- a/Makefile +++ b/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 diff --git a/docs/examples/Makefile b/docs/examples/Makefile new file mode 100644 index 0000000..5cffc83 --- /dev/null +++ b/docs/examples/Makefile @@ -0,0 +1,3 @@ +SUBDIR=../docs/examples +TESTDIR=../../tests +include $(TESTDIR)/make/subdir.mk diff --git a/docs/examples/abstract/Makefile b/docs/examples/abstract/Makefile new file mode 100644 index 0000000..d456aab --- /dev/null +++ b/docs/examples/abstract/Makefile @@ -0,0 +1,3 @@ +SUBDIR=../docs/examples/abstract +TESTDIR=../../../tests +include $(TESTDIR)/make/subdir.mk diff --git a/docs/examples/demos/Makefile b/docs/examples/demos/Makefile new file mode 100644 index 0000000..ecd71ac --- /dev/null +++ b/docs/examples/demos/Makefile @@ -0,0 +1,3 @@ +SUBDIR=../docs/examples/demos +TESTDIR=../../../tests +include $(TESTDIR)/make/subdir.mk diff --git a/sbysrc/demo3.sby b/docs/examples/demos/memory.sby similarity index 100% rename from sbysrc/demo3.sby rename to docs/examples/demos/memory.sby diff --git a/docs/examples/demos/picorv32_axicheck.sby b/docs/examples/demos/picorv32_axicheck.sby new file mode 100644 index 0000000..61b471a --- /dev/null +++ b/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 + diff --git a/sbysrc/demo2.sby b/docs/examples/demos/up_down_counter.sby similarity index 85% rename from sbysrc/demo2.sby rename to docs/examples/demos/up_down_counter.sby index 1d5639c..cb922eb 100644 --- a/sbysrc/demo2.sby +++ b/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 diff --git a/docs/examples/indinv/Makefile b/docs/examples/indinv/Makefile new file mode 100644 index 0000000..c3bf7ac --- /dev/null +++ b/docs/examples/indinv/Makefile @@ -0,0 +1,3 @@ +SUBDIR=../docs/examples/indinv +TESTDIR=../../../tests +include $(TESTDIR)/make/subdir.mk diff --git a/docs/examples/multiclk/Makefile b/docs/examples/multiclk/Makefile new file mode 100644 index 0000000..b6c5eb7 --- /dev/null +++ b/docs/examples/multiclk/Makefile @@ -0,0 +1,3 @@ +SUBDIR=../docs/examples/multiclk +TESTDIR=../../../tests +include $(TESTDIR)/make/subdir.mk diff --git a/docs/examples/puzzles/Makefile b/docs/examples/puzzles/Makefile new file mode 100644 index 0000000..45293b1 --- /dev/null +++ b/docs/examples/puzzles/Makefile @@ -0,0 +1,3 @@ +SUBDIR=../docs/examples/puzzles +TESTDIR=../../../tests +include $(TESTDIR)/make/subdir.mk diff --git a/docs/examples/quickstart/Makefile b/docs/examples/quickstart/Makefile new file mode 100644 index 0000000..be06194 --- /dev/null +++ b/docs/examples/quickstart/Makefile @@ -0,0 +1,3 @@ +SUBDIR=../docs/examples/quickstart +TESTDIR=../../../tests +include $(TESTDIR)/make/subdir.mk diff --git a/sbysrc/demo1.sby b/sbysrc/demo1.sby deleted file mode 100644 index 6c89f18..0000000 --- a/sbysrc/demo1.sby +++ /dev/null @@ -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 - diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 19a962b..d9e0a5c 100644 --- a/sbysrc/sby.py +++ b/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) diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py index cf782b9..89a68ec 100644 --- a/tests/make/collect_tests.py +++ b/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) diff --git a/tests/make/required_tools.py b/tests/make/required_tools.py index 67b5d2b..203ccd7 100644 --- a/tests/make/required_tools.py +++ b/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 ) diff --git a/tests/make/subdir.mk b/tests/make/subdir.mk index b1f367a..86b680f 100644 --- a/tests/make/subdir.mk +++ b/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)/$@ diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py index 04d2226..5c18aca 100644 --- a/tests/make/test_rules.py +++ b/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) -- 2.30.2