- uses: actions/checkout@v2
- uses: YosysHQ/setup-oss-cad-suite@v1
- name: Run checks
- run: tabbypip install xmlschema && make ci
+ run: tabbypip install xmlschema && make ci NOSKIP=1
PYTHON = $(shell cygpath -w -m $(PREFIX)/bin/python3)
endif
+.PHONY: help install ci test html clean
+
help:
@echo ""
@echo "sudo make install"
@echo " build documentation in docs/build/html/"
@echo ""
@echo "make test"
- @echo " run examples"
+ @echo " run tests"
+ @echo ""
+ @echo "make ci"
+ @echo " run tests and check examples"
+ @echo " note: this requires a full Tabby CAD Suite or OSS CAD Suite install"
@echo ""
@echo "make clean"
@echo " cleanup"
chmod +x $(DESTDIR)$(PREFIX)/bin/sby
endif
-ci: \
+.PHONY: check_cad_suite run_ci
+
+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_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 \
- run_tests
+ test
if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
- YOSYS_NOVERIFIC=1 $(MAKE) ci; \
+ YOSYS_NOVERIFIC=1 $(MAKE) run_ci; \
+ fi
+
+check_cad_suite:
+ @if ! which tabbypip >/dev/null 2>&1; then \
+ echo "'make ci' requries the Tabby CAD Suite or the OSS CAD Suite"; \
+ echo "try 'make test' instead or run 'make run_ci' to proceed anyway."; \
+ exit 1; \
fi
test_demo1:
test_quickstart_memory:
cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f memory.sby
-run_tests:
+test:
$(MAKE) -C tests test
html:
.PHONY: test clean refresh help
+TOOL_LIST := \
+ btorsim \
+ yices \
+ aigbmc \
+ avy \
+ bitwuzla \
+ boolector \
+ btormc \
+ cvc4 \
+ mathsat \
+ pono \
+ suprove \
+ yices-smt2 \
+ yices \
+ yosys-abc \
+ z3
+
help:
@cat make/help.txt
python3 make/test_rules.py $<
ifneq (help,$(MAKECMDGOALS))
+
+# This should run every time but only trigger anything depending on it whenever
+# the script overwrites make/rules/found_tools. This doesn't really match how
+# make targets usually work, so we manually shell out here.
+
+FIND_TOOLS := $(shell python3 make/required_tools.py || echo error)
+
+ifneq (,$(findstring error,$(FIND_TOOLS)))
+$(error could not run 'python3 make/required_tools.py')
+endif
+
+ifneq (,$(FIND_TOOLS))
+$(warning $(FIND_TOOLS))
+endif
+
include make/rules/collect.mk
+
endif
-from xmlschema import XMLSchema, XMLSchemaValidationError
+try:
+ from xmlschema import XMLSchema, XMLSchemaValidationError
+except ImportError:
+ import os
+ if "NOSKIP" not in os.environ.get("MAKEFLAGS", ""):
+ print()
+ print("SKIPPING python library xmlschema not found, skipping JUnit output validation")
+ print()
+ exit(0)
+
import argparse
def main():
--- /dev/null
+import shutil
+
+REQUIRED_TOOLS = {
+ ("smtbmc", "yices"): ["yices-smt2"],
+ ("smtbmc", "z3"): ["z3"],
+ ("smtbmc", "cvc4"): ["cvc4"],
+ ("smtbmc", "mathsat"): ["mathsat"],
+ ("smtbmc", "boolector"): ["boolector"],
+ ("smtbmc", "bitwuzla"): ["bitwuzla"],
+ ("smtbmc", "abc"): ["yosys-abc"],
+ ("aiger", "suprove"): ["suprove", "yices"],
+ ("aiger", "avy"): ["avy", "yices"],
+ ("aiger", "aigbmc"): ["aigbmc", "yices"],
+ ("btor", "btormc"): ["btormc", "btorsim"],
+ ("btor", "pono"): ["pono", "btorsim"],
+ ("abc"): ["yices"],
+}
+
+
+def found_tools():
+ with open("make/rules/found_tools") as found_tools_file:
+ return [tool.strip() for tool in found_tools_file.readlines()]
+
+
+if __name__ == "__main__":
+ import subprocess
+ import sys
+ import os
+ from pathlib import Path
+
+ args = sys.argv[1:]
+
+ if args and args[0] == "run":
+ target, command, *required_tools = args[1:]
+
+ with open("make/rules/found_tools") as found_tools_file:
+ found_tools = set(tool.strip() for tool in found_tools_file.readlines())
+
+ missing_tools = sorted(
+ f"`{tool}`" for tool in required_tools if tool not in found_tools
+ )
+ if missing_tools:
+ noskip = "NOSKIP" in os.environ.get("MAKEFLAGS", "")
+ print()
+ print(f"SKIPPING {target}: {', '.join(missing_tools)} not found")
+ if noskip:
+ print("NOSKIP was set, treating this as an error")
+ print()
+ exit(noskip)
+
+ print(command, flush=True)
+ exit(subprocess.call(command, shell=True))
+
+ found_tools = []
+ check_tools = set()
+ for tools in REQUIRED_TOOLS.values():
+ check_tools.update(tools)
+
+ for tool in sorted(check_tools):
+ if not shutil.which(tool):
+ continue
+
+ if tool == "btorsim":
+ error_msg = subprocess.run(
+ ["btorsim", "--vcd"],
+ capture_output=True,
+ text=True,
+ ).stderr
+ if "invalid command line option" in error_msg:
+ print(
+ "found `btorsim` binary is too old "
+ "to support the `--vcd` option, ignoring"
+ )
+ continue
+
+ found_tools.append(tool)
+
+ found_tools = "\n".join(found_tools + [""])
+
+ try:
+ with open("make/rules/found_tools") as found_tools_file:
+ if found_tools_file.read() == found_tools:
+ exit(0)
+ except FileNotFoundError:
+ pass
+
+ Path("make/rules").mkdir(exist_ok=True)
+
+ with open("make/rules/found_tools", "w") as found_tools_file:
+ found_tools_file.write(found_tools)
-import shutil
import sys
import os
import subprocess
import json
+import shlex
from pathlib import Path
+from required_tools import REQUIRED_TOOLS
sby_file = Path(sys.argv[1])
sby_dir = sby_file.parent
return engine, default_solvers.get(engine)
-REQUIRED_TOOLS = {
- ("smtbmc", "yices"): ["yices-smt2"],
- ("smtbmc", "z3"): ["z3"],
- ("smtbmc", "cvc4"): ["cvc4"],
- ("smtbmc", "mathsat"): ["mathsat"],
- ("smtbmc", "boolector"): ["boolector"],
- ("smtbmc", "bitwuzla"): ["bitwuzla"],
- ("smtbmc", "abc"): ["yosys-abc"],
- ("aiger", "suprove"): ["suprove"],
- ("aiger", "avy"): ["avy"],
- ("aiger", "aigbmc"): ["aigbmc"],
- ("btor", "btormc"): ["btormc"],
- ("btor", "pono"): ["pono"],
-}
-
rules_file = Path("make/rules/test") / sby_dir / (sby_file.name + ".mk")
rules_file.parent.mkdir(exist_ok=True, parents=True)
for engine in info["engines"]:
engine, solver = parse_engine(engine)
engines.add(engine)
- required_tools.update(REQUIRED_TOOLS.get((engine, solver), ()))
+ required_tools.update(
+ REQUIRED_TOOLS.get((engine, solver), REQUIRED_TOOLS.get(engine, ()))
+ )
if solver:
solvers.add(solver)
engine_solvers.add((engine, solver))
+ required_tools = sorted(required_tools)
+
print(f".PHONY: {target}", file=rules)
print(f"{target}:", file=rules)
shell_script = sby_dir / f"{sby_file.stem}.sh"
- missing_tools = sorted(
- f"`{tool}`" for tool in required_tools if shutil.which(tool) is None
- )
-
- if missing_tools:
- print(
- f"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; echo",
- file=rules,
- )
-
- elif shell_script.exists():
- print(
- f"\tcd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}",
- file=rules,
- )
+ if shell_script.exists():
+ command = f"cd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}"
else:
- print(
- f"\tcd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}",
- file=rules,
- )
+ command = f"cd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}"
+
+ print(f"\t@python3 make/required_tools.py run {target} {shlex.quote(command)} {shlex.join(required_tools)}", file=rules)
print(f".PHONY: clean-{target}", file=rules)
print(f"clean-{target}:", file=rules)
projects / SymbiYosys.git / commitdiff