Tests for `--keep-going`

This also changes the test Makefile to run `.check.py` files after
running the corresponding `.sby` file to allow more precise testing of
the keep going feature.

diff --git a/tests/.gitignore b/tests/.gitignore
index 212f4ddbe1f3e25fcc3abb967ed421e5905ef440..86d3851aaf89cdb7e4f1dad49f9beff9dee019f6 100644 (file)
--- a/tests/.gitignore
+++ b/tests/.gitignore
@@ -8,5 +8,6 @@
 /redxor*/
 /stopfirst*/
 /junit_*/
+/keepgoing_*/
 /submod_props*/
 /multi_assert*/

diff --git a/tests/Makefile b/tests/Makefile
index 8f1d00c5bc5ebdc3503a799a518874bec85ae1e3..46ec23b291a8b8fa371fb4961ad49ba03b4dc20f 100644 (file)
--- 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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
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)