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
diff --git a/docs/source/autotune.rst b/docs/source/autotune.rst
index 6fab860..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,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.
+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 ``sby
---autotune`` output into the ``[engines]`` section of your ``.sby`` file.
+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
@@ -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
@@ -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
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():
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 6be86a0..3462c36 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -176,13 +176,57 @@ 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)
self.running = True
return
+ 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)
+ self.running = False
+ self.exited = True
+
+ 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(returncode)
+ self.terminated = True
+ self.task.proc_failed(self)
+ return
+
+ 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(returncode)
+ self.terminated = True
+ self.task.proc_failed(self)
+ return
+
+ self.handle_exit(returncode)
+
+ self.finished = True
+ for next_proc in self.notify:
+ next_proc.poll()
+ return
+
+ def read_output(self):
while True:
outs = self.p.stdout.readline().decode("utf-8")
if len(outs) == 0: break
@@ -193,36 +237,6 @@ class SbyProc:
self.linebuffer = ""
self.handle_output(outs)
- if self.p.poll() is not None:
- if not self.silent:
- self.task.log(f"{self.info}: finished (returncode={self.p.returncode})")
- self.task.update_proc_stopped(self)
- self.running = False
- self.exited = True
-
- if self.p.returncode == 127:
- if not self.silent:
- self.task.log(f"{self.info}: COMMAND NOT FOUND. ERROR.")
- self.handle_error(self.p.returncode)
- self.terminated = True
- self.task.proc_failed(self)
- return
-
- if self.checkretcode and self.p.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.terminated = True
- self.task.proc_failed(self)
- return
-
- self.handle_exit(self.p.returncode)
-
- self.finished = True
- for next_proc in self.notify:
- next_proc.poll()
- return
-
class SbyAbort(BaseException):
pass
@@ -552,7 +566,8 @@ 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):
+ print("scc -select; simplemap; select -clear", file=f)
if self.opt_multiclock:
print("clk2fflogic", file=f)
else:
@@ -569,7 +584,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:
@@ -577,7 +592,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)
@@ -610,7 +625,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)
@@ -643,7 +658,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:
@@ -653,7 +668,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)
@@ -675,7 +690,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/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]}.")
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/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"],
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)
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
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
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
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