mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-06 14:24:08 +00:00
Code Activity

Merge pull request #175 from jix/more-test-improvements

Browse source 
Use the test Makefile for all examples
This commit is contained in:
Jannis Harder 2022-06-13 13:59:31 +02:00 committed by GitHub
parent 1d21513a47 499371fd39
commit c50bd781ab
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
18 changed files with 77 additions and 92 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/ci.yml vendored
View file

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

67
Makefile
View file

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

3
docs/examples/Makefile Normal file
View file

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

3
docs/examples/abstract/Makefile Normal file
View file

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

3
docs/examples/demos/Makefile Normal file
View file

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

0
sbysrc/demo3.sby → docs/examples/demos/memory.sby
View file

25
docs/examples/demos/picorv32_axicheck.sby Normal file
View file

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

9
sbysrc/demo2.sby → docs/examples/demos/up_down_counter.sby
View file

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

3
docs/examples/indinv/Makefile Normal file
View file

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

3
docs/examples/multiclk/Makefile Normal file
View file

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

3
docs/examples/puzzles/Makefile Normal file
View file

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

3
docs/examples/quickstart/Makefile Normal file
View file

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

21
sbysrc/demo1.sby
View file

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

1
sbysrc/sby.py
View file

@ -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)

1
tests/make/collect_tests.py
View file

@ -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)

9
tests/make/required_tools.py
View file

@ -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
)

10
tests/make/subdir.mk
View file

@ -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)/$@

3
tests/make/test_rules.py
View file

@ -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)