diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index a9c5c80..18cfb09 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -31,11 +31,12 @@ def run(mode, task, engine_idx, engine):
progress = False
basecase_only = False
induction_only = False
+ keep_going = False
random_seed = None
task.precise_prop_status = True
opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
- "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="])
+ "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "keep-going", "seed="])
for o, a in opts:
if o == "--nomem":
@@ -66,6 +67,10 @@ def run(mode, task, engine_idx, engine):
if basecase_only:
task.error("smtbmc options --basecase and --induction are exclusive.")
induction_only = True
+ elif o == "--keep-going":
+ if mode not in ("bmc", "prove", "prove_basecase", "prove_induction"):
+ task.error("smtbmc option --keep-going is only supported in bmc and prove mode.")
+ keep_going = True
elif o == "--seed":
random_seed = a
else:
@@ -126,6 +131,10 @@ def run(mode, task, engine_idx, engine):
smtbmc_opts.append("-c")
trace_prefix += "%"
+ if keep_going:
+ smtbmc_opts.append("--keep-going")
+ trace_prefix += "%"
+
if dumpsmt2:
smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"]
diff --git a/tests/.gitignore b/tests/.gitignore
index 120675b..23d0008 100644
--- a/tests/.gitignore
+++ b/tests/.gitignore
@@ -8,6 +8,7 @@
/redxor*/
/stopfirst*/
/junit_*/
+/keepgoing_*/
/submod_props*/
/multi_assert*/
/aim_vs_smt2_nonzero_start_offset*/
diff --git a/tests/Makefile b/tests/Makefile
index 8f1d00c..46ec23b 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,16 +1,21 @@
SBY_FILES=$(wildcard *.sby)
SBY_TESTS=$(addprefix test_,$(SBY_FILES:.sby=))
+CHECK_PY_FILES=$(wildcard *.check.py)
+CHECK_PY_TASKS=$(addprefix check_,$(CHECK_PY_FILES:.check.py=))
JUNIT_TESTS=junit_assert_pass junit_assert_fail junit_assert_preunsat \
junit_cover_pass junit_cover_uncovered junit_cover_assert junit_cover_preunsat \
junit_timeout_error_timeout junit_timeout_error_syntax junit_timeout_error_solver
.PHONY: test validate_junit
-test: $(JUNIT_TESTS)
+test: $(JUNIT_TESTS) $(CHECK_PY_TASKS)
test_%: %.sby FORCE
python3 ../sbysrc/sby.py -f $<
+$(CHECK_PY_TASKS): check_%: %.check.py test_%
+ python3 $<
+
$(JUNIT_TESTS): $(SBY_TESTS)
python3 validate_junit.py $@/$@.xml
diff --git a/tests/check_output.py b/tests/check_output.py
new file mode 100644
index 0000000..ab531eb
--- /dev/null
+++ b/tests/check_output.py
@@ -0,0 +1,17 @@
+import re
+
+
+def line_ref(dir, filename, pattern):
+ with open(dir + "/src/" + filename) as file:
+ if isinstance(pattern, str):
+ pattern_re = re.compile(re.escape(pattern))
+ else:
+ pattern_re = pattern
+ pattern = pattern.pattern
+
+ for number, line in enumerate(file, 1):
+ if pattern_re.search(line):
+ # Needs to match source locations for both verilog frontends
+ return fr"{filename}:(?:{number}|\d+.\d+-{number}.\d+)"
+
+ raise RuntimeError("%s: pattern `%s` not found" % (filename, pattern))
diff --git a/tests/keepgoing_multi_step.check.py b/tests/keepgoing_multi_step.check.py
new file mode 100644
index 0000000..0b7d49e
--- /dev/null
+++ b/tests/keepgoing_multi_step.check.py
@@ -0,0 +1,27 @@
+from check_output import *
+
+src = "keepgoing_multi_step.sv"
+
+for task in ["keepgoing_multi_step_bmc", "keepgoing_multi_step_prove"]:
+ assert_0 = line_ref(task, src, "assert(0)")
+ step_3_7 = line_ref(task, src, "step 3,7")
+ step_5 = line_ref(task, src, "step 5")
+ step_7 = line_ref(task, src, "step 7")
+
+ log = open(task + "/logfile.txt").read()
+ log_per_trace = log.split("Writing trace to VCD file")[:-1]
+
+ assert len(log_per_trace) == 4
+
+
+ assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M)
+
+ for i in range(1, 4):
+ assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[i], re.M)
+
+
+ assert re.search(r"Assert failed in test: %s \(.*\)$" % step_3_7, log_per_trace[1], re.M)
+ assert re.search(r"Assert failed in test: %s \(.*\)$" % step_5, log_per_trace[2], re.M)
+ assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M)
+ assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M)
+
diff --git a/tests/keepgoing_multi_step.sby b/tests/keepgoing_multi_step.sby
new file mode 100644
index 0000000..b9b0ba5
--- /dev/null
+++ b/tests/keepgoing_multi_step.sby
@@ -0,0 +1,18 @@
+[tasks]
+bmc
+prove
+
+[options]
+bmc: mode bmc
+prove: mode prove
+expect fail
+
+[engines]
+smtbmc --keep-going boolector
+
+[script]
+read -sv keepgoing_multi_step.sv
+prep -top test
+
+[files]
+keepgoing_multi_step.sv
diff --git a/tests/keepgoing_multi_step.sv b/tests/keepgoing_multi_step.sv
new file mode 100644
index 0000000..8d5d8e3
--- /dev/null
+++ b/tests/keepgoing_multi_step.sv
@@ -0,0 +1,22 @@
+module test (
+ input clk, a
+);
+ reg [7:0] counter = 0;
+
+ always @(posedge clk) begin
+ counter <= counter + 1;
+ end
+
+ always @(posedge clk) begin
+ assert(0);
+ if (counter == 3 || counter == 7) begin
+ assert(a); // step 3,7
+ end
+ if (counter == 5) begin
+ assert(a); // step 5
+ end
+ if (counter == 7) begin
+ assert(a); // step 7
+ end
+ end
+endmodule
diff --git a/tests/keepgoing_same_step.check.py b/tests/keepgoing_same_step.check.py
new file mode 100644
index 0000000..35cd314
--- /dev/null
+++ b/tests/keepgoing_same_step.check.py
@@ -0,0 +1,18 @@
+from check_output import *
+
+task = "keepgoing_same_step"
+src = "keepgoing_same_step.sv"
+
+assert_a = line_ref(task, src, "assert(a)")
+assert_not_a = line_ref(task, src, "assert(!a)")
+assert_0 = line_ref(task, src, "assert(0)")
+
+log = open(task + "/logfile.txt").read()
+log_per_trace = log.split("Writing trace to VCD file")[:-1]
+
+assert len(log_per_trace) == 2
+
+assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_a, log, re.M)
+assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_not_a, log, re.M)
+assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M)
+assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[1], re.M)
diff --git a/tests/keepgoing_same_step.sby b/tests/keepgoing_same_step.sby
new file mode 100644
index 0000000..d344dcc
--- /dev/null
+++ b/tests/keepgoing_same_step.sby
@@ -0,0 +1,13 @@
+[options]
+mode bmc
+expect fail
+
+[engines]
+smtbmc --keep-going boolector
+
+[script]
+read -sv keepgoing_same_step.sv
+prep -top test
+
+[files]
+keepgoing_same_step.sv
diff --git a/tests/keepgoing_same_step.sv b/tests/keepgoing_same_step.sv
new file mode 100644
index 0000000..98fe6d0
--- /dev/null
+++ b/tests/keepgoing_same_step.sv
@@ -0,0 +1,17 @@
+module test (
+ input clk, a
+);
+ reg [7:0] counter = 0;
+
+ always @(posedge clk) begin
+ counter <= counter + 1;
+ end
+
+ always @(posedge clk) begin
+ if (counter == 3) begin
+ assert(a);
+ assert(!a);
+ assert(0);
+ end
+ end
+endmodule
diff --git a/tests/keepgoing_smtc.check.py b/tests/keepgoing_smtc.check.py
new file mode 100644
index 0000000..5749e3f
--- /dev/null
+++ b/tests/keepgoing_smtc.check.py
@@ -0,0 +1,24 @@
+from check_output import *
+
+task = "keepgoing_smtc"
+src = "keepgoing_same_step.sv"
+
+assert_a = line_ref(task, src, "assert(a)")
+assert_not_a = line_ref(task, src, "assert(!a)")
+assert_0 = line_ref(task, src, "assert(0)")
+
+assert_false = line_ref(task, "extra.smtc", "assert false")
+assert_distinct = line_ref(task, "extra.smtc", "assert (distinct")
+
+log = open(task + "/logfile.txt").read()
+log_per_trace = log.split("Writing trace to VCD file")[:-1]
+
+assert len(log_per_trace) == 4
+
+assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_a, log, re.M)
+assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_not_a, log, re.M)
+
+assert re.search(r"Assert src/%s failed: false" % assert_false, log_per_trace[0], re.M)
+assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[1], re.M)
+assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[2], re.M)
+assert re.search(r"Assert src/%s failed: \(distinct" % assert_distinct, log_per_trace[3], re.M)
diff --git a/tests/keepgoing_smtc.sby b/tests/keepgoing_smtc.sby
new file mode 100644
index 0000000..a4cc762
--- /dev/null
+++ b/tests/keepgoing_smtc.sby
@@ -0,0 +1,19 @@
+[options]
+mode bmc
+expect fail
+
+[engines]
+smtbmc --keep-going boolector -- --smtc src/extra.smtc
+
+[script]
+read -sv keepgoing_same_step.sv
+prep -top test
+
+[files]
+keepgoing_same_step.sv
+
+[file extra.smtc]
+state 2
+assert false
+always
+assert (distinct [counter] #b00000111)