From 2d3d96478a001f9686d185ecf26373a29bc52b4d Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 24 Mar 2022 16:36:59 +0100 Subject: [PATCH] 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. --- tests/.gitignore | 1 + tests/Makefile | 7 ++++++- tests/check_output.py | 17 +++++++++++++++++ tests/keepgoing_multi_step.check.py | 27 +++++++++++++++++++++++++++ tests/keepgoing_multi_step.sby | 18 ++++++++++++++++++ tests/keepgoing_multi_step.sv | 22 ++++++++++++++++++++++ tests/keepgoing_same_step.check.py | 18 ++++++++++++++++++ tests/keepgoing_same_step.sby | 13 +++++++++++++ tests/keepgoing_same_step.sv | 17 +++++++++++++++++ tests/keepgoing_smtc.check.py | 24 ++++++++++++++++++++++++ tests/keepgoing_smtc.sby | 19 +++++++++++++++++++ 11 files changed, 182 insertions(+), 1 deletion(-) create mode 100644 tests/check_output.py create mode 100644 tests/keepgoing_multi_step.check.py create mode 100644 tests/keepgoing_multi_step.sby create mode 100644 tests/keepgoing_multi_step.sv create mode 100644 tests/keepgoing_same_step.check.py create mode 100644 tests/keepgoing_same_step.sby create mode 100644 tests/keepgoing_same_step.sv create mode 100644 tests/keepgoing_smtc.check.py create mode 100644 tests/keepgoing_smtc.sby diff --git a/tests/.gitignore b/tests/.gitignore index 212f4dd..86d3851 100644 --- 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 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) -- 2.30.2