- 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
@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"
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
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
--- /dev/null
+SUBDIR=../docs/examples
+TESTDIR=../../tests
+include $(TESTDIR)/make/subdir.mk
--- /dev/null
+SUBDIR=../docs/examples/abstract
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk
--- /dev/null
+SUBDIR=../docs/examples/demos
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk
--- /dev/null
+[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
--- /dev/null
+[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
+
--- /dev/null
+[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
--- /dev/null
+SUBDIR=../docs/examples/indinv
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk
--- /dev/null
+SUBDIR=../docs/examples/multiclk
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk
--- /dev/null
+SUBDIR=../docs/examples/puzzles
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk
--- /dev/null
+SUBDIR=../docs/examples/quickstart
+TESTDIR=../../../tests
+include $(TESTDIR)/make/subdir.mk
+++ /dev/null
-
-[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
-
+++ /dev/null
-[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
+++ /dev/null
-[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
taskinfo[taskname or ""] = {
"mode": cfg.options.get("mode"),
"engines": cfg.engines,
+ "script": cfg.script,
}
print(json.dumps(taskinfo, indent=2))
sys.exit(0)
collect(Path("."))
+collect(Path("../docs/examples"))
out_file = Path("make/rules/collect.mk")
out_file.parent.mkdir(exist_ok=True)
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
)
+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)/$@
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)
projects / SymbiYosys.git / commitdiff