Merge pull request #147 from jix/smtbmc-keepgoing

Support and tests for smtbmc `--keep-going`

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"]
 

tests/.gitignore

@@ -8,6 +8,7 @@
 /redxor*/
 /stopfirst*/
 /junit_*/
+/keepgoing_*/
 /submod_props*/
 /multi_assert*/
 /aim_vs_smt2_nonzero_start_offset*/

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
 

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))

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)
+

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

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

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)

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

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

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)

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)