From: Jannis Harder Date: Mon, 13 Jun 2022 11:20:33 +0000 (+0200) Subject: Use the test Makefile for all examples X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=499371fd39075915fe1a4ac83164e4e426c40d78;p=SymbiYosys.git 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 --- 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/docs/examples/demos/memory.sby b/docs/examples/demos/memory.sby new file mode 100644 index 0000000..c959d88 --- /dev/null +++ b/docs/examples/demos/memory.sby @@ -0,0 +1,53 @@ +[options] +depth 10 +mode bmc + +[engines] +smtbmc yices + +[script] +read_verilog -formal demo.v +prep -top top + +[file demo.v] +module top ( + input clk, + input [7:0] addr, + input [7:0] wdata, + output [7:0] rdata +); + rand const reg [7:0] test_addr; + reg [7:0] test_data; + reg test_valid = 0; + + always @(posedge clk) begin + if (addr == test_addr) begin + if (test_valid) + assert(test_data == rdata); + test_data <= wdata; + test_valid <= 1; + end + end + + memory uut ( + .clk (clk ), + .addr (addr ), + .wdata(wdata), + .rdata(rdata) + ); +endmodule + + +module memory ( + input clk, + input [7:0] addr, + input [7:0] wdata, + output [7:0] rdata +); + reg [7:0] mem [0:255]; + + always @(posedge clk) + mem[addr] <= wdata; + + assign rdata = mem[addr]; +endmodule 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/docs/examples/demos/up_down_counter.sby b/docs/examples/demos/up_down_counter.sby new file mode 100644 index 0000000..cb922eb --- /dev/null +++ b/docs/examples/demos/up_down_counter.sby @@ -0,0 +1,24 @@ +[tasks] +suprove +avy + +[options] +mode prove + +[engines] +suprove: aiger suprove +avy: aiger avy + +[script] +read_verilog -formal demo.v +prep -top top + +[file demo.v] +module top(input clk, input up, down); + reg [4:0] counter = 0; + always @(posedge clk) begin + if (up && counter != 10) counter <= counter + 1; + if (down && counter != 0) counter <= counter - 1; + end + assert property (counter != 15); +endmodule 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/demo2.sby b/sbysrc/demo2.sby deleted file mode 100644 index 1d5639c..0000000 --- a/sbysrc/demo2.sby +++ /dev/null @@ -1,21 +0,0 @@ -[options] -mode prove -wait on - -[engines] -aiger suprove -aiger avy - -[script] -read_verilog -formal demo.v -prep -top top - -[file demo.v] -module top(input clk, input up, down); - reg [4:0] counter = 0; - always @(posedge clk) begin - if (up && counter != 10) counter <= counter + 1; - if (down && counter != 0) counter <= counter - 1; - end - assert property (counter != 15); -endmodule diff --git a/sbysrc/demo3.sby b/sbysrc/demo3.sby deleted file mode 100644 index c959d88..0000000 --- a/sbysrc/demo3.sby +++ /dev/null @@ -1,53 +0,0 @@ -[options] -depth 10 -mode bmc - -[engines] -smtbmc yices - -[script] -read_verilog -formal demo.v -prep -top top - -[file demo.v] -module top ( - input clk, - input [7:0] addr, - input [7:0] wdata, - output [7:0] rdata -); - rand const reg [7:0] test_addr; - reg [7:0] test_data; - reg test_valid = 0; - - always @(posedge clk) begin - if (addr == test_addr) begin - if (test_valid) - assert(test_data == rdata); - test_data <= wdata; - test_valid <= 1; - end - end - - memory uut ( - .clk (clk ), - .addr (addr ), - .wdata(wdata), - .rdata(rdata) - ); -endmodule - - -module memory ( - input clk, - input [7:0] addr, - input [7:0] wdata, - output [7:0] rdata -); - reg [7:0] mem [0:255]; - - always @(posedge clk) - mem[addr] <= wdata; - - assign rdata = mem[addr]; -endmodule 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)