From db740839b737ee55b8b39f1b29780872d32d248a Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Wed, 22 Jun 2022 21:17:29 -0700 Subject: [PATCH 01/14] switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules. Fixes: #168 Depends on: https://github.com/YosysHQ/yosys/pull/3391 --- sbysrc/sby_core.py | 12 ++++++------ tests/unsorted/blackbox.sby | 31 ++++++++++++++++++++++++++++++ tests/unsorted/smtlib2_module.sby | 32 +++++++++++++++++++++++++++++++ 3 files changed, 69 insertions(+), 6 deletions(-) create mode 100644 tests/unsorted/blackbox.sby create mode 100644 tests/unsorted/smtlib2_module.sby diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index ab10614..3592c31 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -465,7 +465,7 @@ class SbyTask(SbyConfig): if not os.path.isdir(f"{self.workdir}/model"): os.makedirs(f"{self.workdir}/model") - def print_common_prep(): + def print_common_prep(check): if self.opt_multiclock: print("clk2fflogic", file=f) else: @@ -482,7 +482,7 @@ class SbyTask(SbyConfig): print("setundef -anyseq", file=f) print("opt -keepdc -fast", file=f) print("check", file=f) - print("hierarchy -simcheck", file=f) + print(f"hierarchy {check}", file=f) if model_name == "base": with open(f"""{self.workdir}/model/design.ys""", "w") as f: @@ -490,7 +490,7 @@ class SbyTask(SbyConfig): for cmd in self.script: print(cmd, file=f) # the user must designate a top module in [script] - print("hierarchy -simcheck", file=f) + print("hierarchy -smtcheck", file=f) print(f"""write_jny -no-connections ../model/design.json""", file=f) print(f"""write_rtlil ../model/design.il""", file=f) @@ -522,7 +522,7 @@ class SbyTask(SbyConfig): print("memory_map", file=f) else: print("memory_nordff", file=f) - print_common_prep() + print_common_prep("-smtcheck") if "_syn" in model_name: print("techmap", file=f) print("opt -fast", file=f) @@ -555,7 +555,7 @@ class SbyTask(SbyConfig): print("memory_map", file=f) else: print("memory_nordff", file=f) - print_common_prep() + print_common_prep("-simcheck") print("flatten", file=f) print("setundef -undriven -anyseq", file=f) if "_syn" in model_name: @@ -587,7 +587,7 @@ class SbyTask(SbyConfig): print(f"# running in {self.workdir}/model/", file=f) print("read_ilang design.il", file=f) print("memory_map", file=f) - print_common_prep() + print_common_prep("-simcheck") print("flatten", file=f) print("setundef -undriven -anyseq", file=f) print("setattr -unset keep", file=f) diff --git a/tests/unsorted/blackbox.sby b/tests/unsorted/blackbox.sby new file mode 100644 index 0000000..ca9400e --- /dev/null +++ b/tests/unsorted/blackbox.sby @@ -0,0 +1,31 @@ +[options] +mode bmc +depth 1 +expect error + +[engines] +smtbmc + +[script] +read_verilog -formal test.v +prep -top top + +[file test.v] +(* blackbox *) +module submod(a, b); + input [7:0] a; + output [7:0] b; +endmodule + +module top; + wire [7:0] a = $anyconst, b; + + submod submod( + .a(a), + .b(b) + ); + + always @* begin + assert(~a == b); + end +endmodule diff --git a/tests/unsorted/smtlib2_module.sby b/tests/unsorted/smtlib2_module.sby new file mode 100644 index 0000000..43dfcb2 --- /dev/null +++ b/tests/unsorted/smtlib2_module.sby @@ -0,0 +1,32 @@ +[options] +mode bmc +depth 1 + +[engines] +smtbmc + +[script] +read_verilog -formal test.v +prep -top top + +[file test.v] +(* blackbox *) +(* smtlib2_module *) +module submod(a, b); + input [7:0] a; + (* smtlib2_comb_expr = "(bvnot a)" *) + output [7:0] b; +endmodule + +module top; + wire [7:0] a = $anyconst, b; + + submod submod( + .a(a), + .b(b) + ); + + always @* begin + assert(~a == b); + end +endmodule From e01ac8b84855aa7581d40a69d15c42d1432a8432 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 29 Jun 2022 16:43:07 +0200 Subject: [PATCH 02/14] tests: Test for invalid x-value FF init optimizations --- tests/regression/ff_xinit_opt.sby | 39 +++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 tests/regression/ff_xinit_opt.sby diff --git a/tests/regression/ff_xinit_opt.sby b/tests/regression/ff_xinit_opt.sby new file mode 100644 index 0000000..2078ad1 --- /dev/null +++ b/tests/regression/ff_xinit_opt.sby @@ -0,0 +1,39 @@ +[options] +mode bmc + +[engines] +smtbmc boolector + +[script] +read_verilog -formal ff_xinit_opt.sv +prep -flatten -top top + +opt -fast -keepdc + +[file ff_xinit_opt.sv] +module top( + input clk, + input [7:0] d +); + + (* keep *) + wire [7:0] some_const = $anyconst; + + wire [7:0] q1; + wire [7:0] q2; + + ff ff1(.clk(clk), .d(q1), .q(q1)); + ff ff2(.clk(1'b0), .d(d), .q(q2)); + + initial assume (some_const == q1); + initial assume (some_const == q2); + initial assume (q1 != 0); + initial assume (q2 != 0); + + always @(posedge clk) assert(some_const == q1); + always @(posedge clk) assert(some_const == q2); +endmodule + +module ff(input clk, input [7:0] d, (* keep *) output reg [7:0] q); + always @(posedge clk) q <= d; +endmodule From ff802086b4b1b9d9ca0c74fd5fa521b5316bbe4c Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 29 Jun 2022 18:00:52 +0200 Subject: [PATCH 03/14] test uninited FFs with const clks and fix btor script for this --- sbysrc/sby_core.py | 2 +- tests/regression/const_clocks.sby | 43 +++++++++++++++++++++++++++++++ 2 files changed, 44 insertions(+), 1 deletion(-) create mode 100644 tests/regression/const_clocks.sby diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 4e57b21..5580d09 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -653,7 +653,7 @@ class SbyTask(SbyConfig): print("abc", file=f) print("opt_clean", file=f) else: - print("opt -fast", file=f) + print("opt -fast -keepdc", file=f) print("delete -output", file=f) print("dffunmap", file=f) print("stat", file=f) diff --git a/tests/regression/const_clocks.sby b/tests/regression/const_clocks.sby new file mode 100644 index 0000000..245358b --- /dev/null +++ b/tests/regression/const_clocks.sby @@ -0,0 +1,43 @@ +[tasks] +btor +smt +btor_m btor multiclock +smt_m smt multiclock + +[options] +mode bmc + +multiclock: multiclock on + +[engines] +#smtbmc +btor: btor btormc +smt: smtbmc boolector + +[script] +read_verilog -formal const_clocks.sv +prep -flatten -top top + +[file const_clocks.sv] +module top( + input clk, + input [7:0] d +); + + (* keep *) + wire [7:0] some_const = $anyconst; + + wire [7:0] q; + + ff ff1(.clk(1'b0), .d(d), .q(q)); + + initial assume (some_const == q); + initial assume (q != 0); + + + always @(posedge clk) assert(some_const == q); +endmodule + +module ff(input clk, input [7:0] d, (* keep *) output reg [7:0] q); + always @(posedge clk) q <= d; +endmodule From ea7fc7dc2c0d7eea25dabe06beba6ebe56d58c7d Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 5 Jul 2022 15:34:27 +0200 Subject: [PATCH 04/14] tests: Windows fixes Make tests runnable on Windows, as long as a unix like environment as e.g. provided by MSYS2 is available. --- tests/Makefile | 20 ++++++++++++++++++-- tests/make/collect_tests.py | 21 +++++++++++++-------- tests/make/test_rules.py | 25 +++++++++++++++++++------ 3 files changed, 50 insertions(+), 16 deletions(-) diff --git a/tests/Makefile b/tests/Makefile index 9b65da7..805d190 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -2,11 +2,27 @@ test: .PHONY: test clean refresh help +OS_NAME := $(shell python3 -c "import os;print(os.name)") +ifeq (nt,$(OS_NAME)) +ifeq (quoted,$(shell echo "quoted")) +OS_NAME := nt-unix-like +endif +endif + +ifeq (nt,$(OS_NAME)) +$(error This Makefile requires unix-like tools and shell, e.g. MSYS2.) +endif + help: @cat make/help.txt -export SBY_WORKDIR_GITIGNORE=1 -export SBY_MAIN=$(realpath $(dir $(firstword $(MAKEFILE_LIST)))/../sbysrc/sby.py) +export SBY_WORKDIR_GITIGNORE := 1 + +SBY_MAIN := $(realpath $(dir $(firstword $(MAKEFILE_LIST)))/../sbysrc/sby.py) +ifeq (nt-unix-like,$(OS_NAME)) +SBY_MAIN := $(shell cygpath -w $(SBY_MAIN)) +endif +export SBY_MAIN make/rules/collect.mk: make/collect_tests.py python3 make/collect_tests.py diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py index 89a68ec..b5f7699 100644 --- a/tests/make/collect_tests.py +++ b/tests/make/collect_tests.py @@ -4,7 +4,8 @@ import re tests = [] checked_dirs = [] -SAFE_PATH = re.compile(r"^[a-zA-Z0-9_./]*$") +SAFE_PATH = re.compile(r"^[a-zA-Z0-9_./\\]*$") + def collect(path): # don't pick up any paths that need escaping nor any sby workdirs @@ -15,8 +16,6 @@ def collect(path): for entry in path.glob("*.sby"): filename = str(entry) if not SAFE_PATH.match(filename): - continue - if not re.match(r"^[a-zA-Z0-9_./]*$", filename): print(f"skipping {filename!r}, use only [a-zA-Z0-9_./] in filenames") continue tests.append(entry) @@ -25,6 +24,10 @@ def collect(path): collect(entry) +def unix_path(path): + return "/".join(path.parts) + + collect(Path(".")) collect(Path("../docs/examples")) @@ -33,16 +36,18 @@ out_file.parent.mkdir(exist_ok=True) with out_file.open("w") as output: - for checked_dir in checked_dirs: print(f"{out_file}: {checked_dir}", file=output) for test in tests: - print(f"make/rules/test/{test}.mk: {test}", file=output) + test_unix = unix_path(test) + print(f"make/rules/test/{test_unix}.mk: {test_unix}", file=output) for ext in [".sh", ".py"]: script_file = test.parent / (test.stem + ext) if script_file.exists(): - print(f"make/rules/test/{test}.mk: {script_file}", file=output) - print(f"make/rules/test/{test}.mk: make/test_rules.py", file=output) + script_file_unix = unix_path(script_file) + print(f"make/rules/test/{test_unix}.mk: {script_file_unix}", file=output) + print(f"make/rules/test/{test_unix}.mk: make/test_rules.py", file=output) for test in tests: - print(f"-include make/rules/test/{test}.mk", file=output) + test_unix = unix_path(test) + print(f"-include make/rules/test/{test_unix}.mk", file=output) diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py index 5c18aca..9607d81 100644 --- a/tests/make/test_rules.py +++ b/tests/make/test_rules.py @@ -7,6 +7,11 @@ from pathlib import Path from required_tools import REQUIRED_TOOLS + +def unix_path(path): + return "/".join(path.parts) + + sby_file = Path(sys.argv[1]) sby_dir = sby_file.parent @@ -56,7 +61,10 @@ 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"]): + if any( + line.startswith("read -verific") or line.startswith("verific") + for line in info["script"] + ): required_tools.add("verific") required_tools = sorted(required_tools) @@ -66,12 +74,17 @@ with rules_file.open("w") as rules: shell_script = sby_dir / f"{sby_file.stem}.sh" - if shell_script.exists(): - command = f"cd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}" - else: - command = f"cd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}" + sby_dir_unix = unix_path(sby_dir) - print(f"\t@python3 make/required_tools.py run {target} {shlex.quote(command)} {shlex.join(required_tools)}", file=rules) + if shell_script.exists(): + command = f"cd {sby_dir_unix} && env SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}" + else: + command = f"cd {sby_dir_unix} && 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) From 566edad13c369bd4a4f5c7bc61a11b7e5d390493 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 5 Jul 2022 17:20:55 +0200 Subject: [PATCH 05/14] Read config before creating a workdir When using a task name not defined in the config, this now produces an error before creating an unnecessary workdir for that non-existing task. --- sbysrc/sby.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index b802b7a..0628c6d 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -402,6 +402,8 @@ if (workdir is not None) and (len(tasknames) != 1): sys.exit(1) def run_task(taskname): + sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname) + my_opt_tmpdir = opt_tmpdir my_workdir = None @@ -461,7 +463,6 @@ def run_task(taskname): else: junit_filename = "junit" - sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname) task = SbyTask(sbyconfig, my_workdir, early_logmsgs, reusedir) for k, v in exe_paths.items(): From b3b315a473ac6436517ebbfebce24392f2bd3b27 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 6 Jul 2022 11:19:51 +0200 Subject: [PATCH 06/14] Make SbyProc hide Windows differences in retcode handling Without this, we don't properly detect missing solver binaries and do not properly handle the return status of the pono solver. --- sbysrc/sby_core.py | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 5580d09..372cbeb 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -176,7 +176,7 @@ class SbyProc: fcntl.fcntl(self.p.stdout, fcntl.F_SETFL, fl | os.O_NONBLOCK) else: - self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE, + self.p = subprocess.Popen(self.cmdline + " & exit !errorlevel!", shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE, stderr=(subprocess.STDOUT if self.logstderr else None)) self.task.update_proc_running(self) @@ -200,23 +200,31 @@ class SbyProc: self.running = False self.exited = True - if self.p.returncode == 127: + if os.name == "nt": + if self.p.returncode == 9009: + returncode = 127 + else: + returncode = self.p.returncode & 0xff + else: + returncode = self.p.returncode + + if returncode == 127: if not self.silent: self.task.log(f"{self.info}: COMMAND NOT FOUND. ERROR.") - self.handle_error(self.p.returncode) + self.handle_error(returncode) self.terminated = True self.task.proc_failed(self) return - if self.checkretcode and self.p.returncode not in self.retcodes: + if self.checkretcode and returncode not in self.retcodes: if not self.silent: self.task.log(f"{self.info}: task failed. ERROR.") - self.handle_error(self.p.returncode) + self.handle_error(returncode) self.terminated = True self.task.proc_failed(self) return - self.handle_exit(self.p.returncode) + self.handle_exit(returncode) self.finished = True for next_proc in self.notify: From 92e7eb2e3225d7a3bdf23497d80e4901b6c75e98 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 8 Jul 2022 12:36:44 +0200 Subject: [PATCH 07/14] abc pdr: Enable log output by default This makes it consistent with the other abc solvers and shows whether abc pdr is making progress. --- sbysrc/sby_engine_abc.py | 1 + 1 file changed, 1 insertion(+) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 4635ee1..e96ddb8 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -41,6 +41,7 @@ def run(mode, task, engine_idx, engine): elif abc_command[0] == "pdr": if mode != "prove": task.error("ABC command 'pdr' is only valid in prove mode.") + abc_command[0] += f" -v" else: task.error(f"Invalid ABC command {abc_command[0]}.") From bc2bb5c86316ae0e0be9a5431d806c2ce88583d3 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 8 Jul 2022 14:31:57 +0200 Subject: [PATCH 08/14] docs: Don't use linebreaks within inline code spans. --- docs/source/autotune.rst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/docs/source/autotune.rst b/docs/source/autotune.rst index 6fab860..7ef07c1 100644 --- a/docs/source/autotune.rst +++ b/docs/source/autotune.rst @@ -11,15 +11,15 @@ Using Autotune -------------- To run autotune, you can add the ``--autotune`` option to your usual sby -invokation. For example if you usually run ``sby demo.sby`` you would run ``sby ---autotune demo.sby`` instead. When the ``.sby`` file contains multiple tasks, -autotune is run for each task independently. As without ``--autotune``, it is -possible to specify which tasks to run on the command line. +invokation. For example if you usually run ``sby demo.sby`` you would run +``sby --autotune demo.sby`` instead. When the ``.sby`` file contains multiple +tasks, autotune is run for each task independently. As without ``--autotune``, +it is possible to specify which tasks to run on the command line. Autotune runs without requiring further interaction and will eventually print a list of engine configurations and their respective solving times. To -permanently use an engine configuration you can copy if from the ``sby ---autotune`` output into the ``[engines]`` section of your ``.sby`` file. +permanently use an engine configuration you can copy if from the +``sby --autotune`` output into the ``[engines]`` section of your ``.sby`` file. Autotune Log Output ------------------- @@ -112,8 +112,8 @@ their solving time: If any tried engine encounters an error or produces an unexpected result, autotune will also output a list of failed engines. Note that when the sby file -does not contain the ``expect`` option, autotune defaults to ``expect -pass,fail`` to simplify running autotune on a verification task with a +does not contain the ``expect`` option, autotune defaults to +``expect pass,fail`` to simplify running autotune on a verification task with a currently unknown outcome. Configuring Autotune From 4ab610ce87e02d3340989c46d92cc513827b53fc Mon Sep 17 00:00:00 2001 From: matt venn Date: Mon, 11 Jul 2022 11:10:45 +0200 Subject: [PATCH 09/14] Update autotune.rst --- docs/source/autotune.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/autotune.rst b/docs/source/autotune.rst index 7ef07c1..d61f996 100644 --- a/docs/source/autotune.rst +++ b/docs/source/autotune.rst @@ -11,7 +11,7 @@ Using Autotune -------------- To run autotune, you can add the ``--autotune`` option to your usual sby -invokation. For example if you usually run ``sby demo.sby`` you would run +invocation. For example if you usually run ``sby demo.sby`` you would run ``sby --autotune demo.sby`` instead. When the ``.sby`` file contains multiple tasks, autotune is run for each task independently. As without ``--autotune``, it is possible to specify which tasks to run on the command line. From ca3429e3286b363584bd797ba397b9c1f6e4b4b7 Mon Sep 17 00:00:00 2001 From: KrystalDelusion <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 11 Jul 2022 21:21:31 +1200 Subject: [PATCH 10/14] Autotune grammar/spelling check --- docs/source/autotune.rst | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/docs/source/autotune.rst b/docs/source/autotune.rst index d61f996..909b838 100644 --- a/docs/source/autotune.rst +++ b/docs/source/autotune.rst @@ -3,7 +3,7 @@ Autotune: Automatic Engine Selection Selecting the best performing engine for a given verification task often requires some amount of trial and error. To reduce the manual work required for -this, sby offers the ``--autotune`` option which takes an ``.sby`` file and +this, sby offers the ``--autotune`` option. This takes an ``.sby`` file and runs it using engines and engine configurations. At the end it produces a report listing the fastest engines among these candidates. @@ -11,14 +11,14 @@ Using Autotune -------------- To run autotune, you can add the ``--autotune`` option to your usual sby -invocation. For example if you usually run ``sby demo.sby`` you would run +invocation. For example, if you usually run ``sby demo.sby`` you would run ``sby --autotune demo.sby`` instead. When the ``.sby`` file contains multiple tasks, autotune is run for each task independently. As without ``--autotune``, it is possible to specify which tasks to run on the command line. -Autotune runs without requiring further interaction and will eventually print a +Autotune runs without requiring further interaction, and will eventually print a list of engine configurations and their respective solving times. To -permanently use an engine configuration you can copy if from the +permanently use an engine configuration you can copy it from the ``sby --autotune`` output into the ``[engines]`` section of your ``.sby`` file. Autotune Log Output @@ -37,9 +37,9 @@ once and will be reused to run every candidate engine. SBY [demo] base: finished (returncode=0) SBY [demo] prepared model 'base' -This is followed by selecting the engine candidates to run. For this the design +This is followed by selecting the engine candidates to run. The design and sby configuration are analyzed to skip engines that are not compatible or -unlikely to work well. When engines is skipped due to a recommendation, a +unlikely to work well. When an engine is skipped due to a recommendation, a corresponding log message is displayed as well as the total number of candidates to try: @@ -49,7 +49,7 @@ candidates to try: SBY [demo] testing 16 engine configurations... After this, the candidate engine configurations are started. Depending on the -configuration engines can run in parallel. The engine output itself is not +configuration, engines can run in parallel. The engine output itself is not logged to stdout when running autotune, so you will only see messages about starting an engine: @@ -77,7 +77,7 @@ be interspersed with other log output. SBY [demo] smt2: finished (returncode=0) SBY [demo] prepared model 'smt2' -Whenever an engine finishes a log message is printed: +Whenever an engine finishes, a log message is printed: .. code-block:: text @@ -91,7 +91,7 @@ When an engine takes longer than the current hard timeout, it is stopped: SBY [demo] engine_2 (smtbmc bitwuzla): timeout (150 seconds) Depending on the configuration, autotune will also stop an engine earlier when -reaching a soft timeout. In that case, when no other engine finishes in less +reaching a soft timeout. If no other engine finishes in less time, the engine will be retried later with a longer soft timeout: .. code-block:: text @@ -99,7 +99,7 @@ time, the engine will be retried later with a longer soft timeout: SBY [demo] engine_0 (smtbmc boolector): timeout (60 seconds, will be retried if necessary) -Finally at the end a summary of all finished engines is printed, sorted by +Finally, a summary of all finished engines is printed, sorted by their solving time: .. code-block:: text @@ -121,7 +121,7 @@ Configuring Autotune Autotune can be configured by adding an ``[autotune]`` section to the ``.sby`` file. Each line in that section has the form ``option_name value``, the -possible options and their supported values are described below. In addition +possible options and their supported values are described below. In addition, the ``--autotune-config`` command line option can be used to specify a file containing further autotune options, using the same syntax. When both are used, the command line option takes precedence. This makes it easy to run autotune From 5d3f784bebd7f952ccfbe8323f6d97b66f2ebf04 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 13 Jul 2022 15:54:24 +0200 Subject: [PATCH 11/14] Fix a race-condition SbyProc that could truncate output Present for a long time, but was not easy to hit. Some of my work in progress changes made this much more likely and running the complete test suite in parallel had a good chance of reproducing this for at least one of the tests. --- sbysrc/sby_core.py | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 372cbeb..391fb16 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -183,17 +183,12 @@ class SbyProc: self.running = True return - while True: - outs = self.p.stdout.readline().decode("utf-8") - if len(outs) == 0: break - if outs[-1] != '\n': - self.linebuffer += outs - break - outs = (self.linebuffer + outs).strip() - self.linebuffer = "" - self.handle_output(outs) + self.read_output() if self.p.poll() is not None: + # The process might have written something since the last time we checked + self.read_output() + if not self.silent: self.task.log(f"{self.info}: finished (returncode={self.p.returncode})") self.task.update_proc_stopped(self) @@ -231,6 +226,17 @@ class SbyProc: next_proc.poll() return + def read_output(self): + while True: + outs = self.p.stdout.readline().decode("utf-8") + if len(outs) == 0: break + if outs[-1] != '\n': + self.linebuffer += outs + break + outs = (self.linebuffer + outs).strip() + self.linebuffer = "" + self.handle_output(outs) + class SbyAbort(BaseException): pass From 3ff2c9affc0bf0e96971960dc9c6bb93325a1566 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Tue, 19 Jul 2022 18:34:43 +0200 Subject: [PATCH 12/14] avoid erroring out when coarse-grain logic loops can be resolved by mapping to fine grain operators --- sbysrc/sby_core.py | 1 + tests/regression/fake_loop.sby | 23 +++++++++++++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 tests/regression/fake_loop.sby diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 391fb16..3462c36 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -567,6 +567,7 @@ class SbyTask(SbyConfig): os.makedirs(f"{self.workdir}/model") def print_common_prep(check): + print("scc -select; simplemap; select -clear", file=f) if self.opt_multiclock: print("clk2fflogic", file=f) else: diff --git a/tests/regression/fake_loop.sby b/tests/regression/fake_loop.sby new file mode 100644 index 0000000..419e267 --- /dev/null +++ b/tests/regression/fake_loop.sby @@ -0,0 +1,23 @@ +[options] +mode cover + +[engines] +smtbmc boolector + +[script] +read -formal fake_loop.sv +hierarchy -top fake_loop +proc + +[file fake_loop.sv] +module fake_loop(input clk, input a, input b, output [9:0] x); + wire [9:0] ripple; + reg [9:0] prev_ripple = 9'b0; + + always @(posedge clk) prev_ripple <= ripple; + + assign ripple = {ripple[8:0], a} ^ prev_ripple; // only cyclic at the coarse-grain level + assign x = ripple[9] + b; + + always @(posedge clk) cover(ripple[9]); +endmodule From 1cf206fc1c73e2323dbaf7e0779b3bb3d0d1a9ce Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Mon, 25 Jul 2022 17:01:17 +0200 Subject: [PATCH 13/14] add cvc5 executable to required tool mapping --- tests/make/required_tools.py | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/make/required_tools.py b/tests/make/required_tools.py index 203ccd7..ce33356 100644 --- a/tests/make/required_tools.py +++ b/tests/make/required_tools.py @@ -4,6 +4,7 @@ REQUIRED_TOOLS = { ("smtbmc", "yices"): ["yices-smt2"], ("smtbmc", "z3"): ["z3"], ("smtbmc", "cvc4"): ["cvc4"], + ("smtbmc", "cvc5"): ["cvc5"], ("smtbmc", "mathsat"): ["mathsat"], ("smtbmc", "boolector"): ["boolector"], ("smtbmc", "bitwuzla"): ["bitwuzla"], From 9293e660920f3c2927f8c920f7e3d651b3265d2f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 26 Jul 2022 16:03:36 +0200 Subject: [PATCH 14/14] example for autotune --- docs/examples/autotune/README.md | 30 +++++++++++ docs/examples/autotune/divider.sby | 24 +++++++++ docs/examples/autotune/divider.sv | 85 ++++++++++++++++++++++++++++++ 3 files changed, 139 insertions(+) create mode 100644 docs/examples/autotune/README.md create mode 100644 docs/examples/autotune/divider.sby create mode 100644 docs/examples/autotune/divider.sv diff --git a/docs/examples/autotune/README.md b/docs/examples/autotune/README.md new file mode 100644 index 0000000..3cdadb7 --- /dev/null +++ b/docs/examples/autotune/README.md @@ -0,0 +1,30 @@ +# Autotune demo + +This directory contains a simple sequential integer divider circuit. The +verilog implementation in [divider.sv](divider.sv) comes with assertions that +this circuit will always produce the correct result and will always finish +within a fixed number of cycles. The circuit has the divider bit-width as +parameter. + +Increasing the WIDTH parameter quickly turns proving those assertions into a +very difficult proof for fully autmated solvers. This makes it a good example +for the `--autotune` option which tries different backend engines to find the +best performing engine configuration for a given verification task. + +The [divider.sby](divider.sby) file defines 3 tasks named `small`, `medium` and +`large` which configure the divider with different bit-widths. To verify the +`small` divider using the default engine run: + + sby -f divider.sby small + +To automatically try different backend engines using autotune, run + + sby --autotune -f divider.sby small + +The `small` task should finish quickly using both the default engine and using +autotune. The `medium` and `large` tasks take significantly longer and show +greater differences between engine configurations. Note that the `large` tasks +can take many minutes to hours, depending on the machine you are using. + +You can learn more about Sby's autotune feature from [Sby's +documentation](https://symbiyosys.readthedocs.io/en/latest/autotune.html). diff --git a/docs/examples/autotune/divider.sby b/docs/examples/autotune/divider.sby new file mode 100644 index 0000000..61bed9a --- /dev/null +++ b/docs/examples/autotune/divider.sby @@ -0,0 +1,24 @@ +[tasks] +small default +medium +large + +[options] +mode prove +small: depth 11 +medium: depth 15 +large: depth 19 + +[engines] +smtbmc + +[script] +small: read -define WIDTH=8 +medium: read -define WIDTH=12 +large: read -define WIDTH=16 + +read -formal divider.sv +prep -top divider + +[files] +divider.sv diff --git a/docs/examples/autotune/divider.sv b/docs/examples/autotune/divider.sv new file mode 100644 index 0000000..b2ec2ad --- /dev/null +++ b/docs/examples/autotune/divider.sv @@ -0,0 +1,85 @@ +`ifndef WIDTH +`define WIDTH 4 +`endif + +module divider #( + parameter WIDTH=`WIDTH +) ( + input wire clk, + input wire start, + input wire [WIDTH-1:0] dividend, + input wire [WIDTH-1:0] divisor, + + output reg done, + output reg [WIDTH-1:0] quotient, + output wire [WIDTH-1:0] remainder +); + + reg [WIDTH-1:0] acc; + + reg [WIDTH*2-1:0] sub; + reg [WIDTH-1:0] pos; + + assign remainder = acc; + + always @(posedge clk) begin + if (start) begin + acc <= dividend; + quotient <= 0; + sub <= divisor << (WIDTH - 1); + pos <= 1 << (WIDTH - 1); + done <= 0; + end else if (!done) begin + if (acc >= sub) begin + acc <= acc - sub[WIDTH-1:0]; + quotient <= quotient + pos; + end + + sub <= sub >> 1; + {pos, done} <= pos; + end + end + + +`ifdef FORMAL + reg [WIDTH-1:0] start_dividend = 0; + reg [WIDTH-1:0] start_divisor = 0; + + reg started = 0; + reg finished = 0; + reg [$clog2(WIDTH + 1):0] counter = 0; + + always @(posedge clk) begin + // Bound the number of cycles until the result is ready + assert (counter <= WIDTH); + + if (started) begin + if (finished || done) begin + finished <= 1; + // Make sure result stays until we start a new division + assert (done); + + // Check the result + if (start_divisor == 0) begin + assert ("ient); + assert (remainder == start_dividend); + end else begin + assert (quotient == start_dividend / start_divisor); + assert (remainder == start_dividend % start_divisor); + end + end else begin + counter <= counter + 1'b1; + end + end + + // Track the requested inputs + if (start) begin + start_divisor <= divisor; + start_dividend <= dividend; + started <= 1; + counter <= 0; + finished <= 0; + end + end +`endif +endmodule