diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 6f9c09c..9fb3278 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -198,6 +198,9 @@ options are: | | | indicated in SBY's log output). | | | | Values: ``on``, ``off``. Default: ``on`` | +-------------------+------------+---------------------------------------------------------+ +| ``cover_assert`` | ``cover`` | Check for assertion properties during ``cover`` mode. | +| | | Values: ``on``, ``off``. Default: ``off`` | ++-------------------+------------+---------------------------------------------------------+ Engines section --------------- diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index c181c18..6e14d6d 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1020,7 +1020,10 @@ class SbyTask(SbyConfig): if self.opt_mode in ["bmc", "prove"]: print("chformal -live -fair -cover -remove", file=f) if self.opt_mode == "cover": - print("chformal -live -fair -remove", file=f) + if self.opt_cover_assert: + print("chformal -live -fair -remove", file=f) + else: + print("chformal -live -fair -assert -remove", file=f) if self.opt_mode == "live": print("chformal -assert2assume", file=f) print("chformal -cover -remove", file=f) @@ -1294,6 +1297,9 @@ class SbyTask(SbyConfig): self.handle_bool_option("skip_prep", False) self.handle_bool_option("assume_early", True) + + if self.opt_mode == "cover": + self.handle_bool_option("cover_assert", False) def setup_status_db(self, status_path=None): if hasattr(self, 'status_db'): diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 24ea00e..fe0380e 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -187,6 +187,7 @@ def run(mode, task, engine_idx, engine): pending_sim = None current_step = None procs_running = 1 + failed_assert = False def output_callback(line): nonlocal proc_status @@ -194,6 +195,7 @@ def run(mode, task, engine_idx, engine): nonlocal pending_sim nonlocal current_step nonlocal procs_running + nonlocal failed_assert if pending_sim: sim_proc = sim_witness_trace(procname, task, engine_idx, pending_sim, append=sim_append, inductive=mode == "prove_induction") @@ -235,6 +237,7 @@ def run(mode, task, engine_idx, engine): match = re.match(r"^## [0-9: ]+ Assert failed in ([^:]+): (\S+)(?: \((\S+)\))?", line) if match: + failed_assert = not keep_going path = parse_mod_path(match[1]) cell_name = match[3] or match[2] prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) @@ -276,7 +279,7 @@ def run(mode, task, engine_idx, engine): pending_sim = tracefile match = re.match(r"^## [0-9: ]+ Unreached cover statement at ([^:]+): (\S+)(?: \((\S+)\))?", line) - if match: + if match and not failed_assert: path = parse_mod_path(match[1]) cell_name = match[3] or match[2] prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) diff --git a/tests/junit/junit_cover.sby b/tests/junit/junit_cover.sby index 53747ba..f853d16 100644 --- a/tests/junit/junit_cover.sby +++ b/tests/junit/junit_cover.sby @@ -7,6 +7,7 @@ preunsat [options] mode cover depth 1 +cover_assert on pass: expect pass fail: expect fail diff --git a/tests/statusdb/Makefile b/tests/statusdb/Makefile new file mode 100644 index 0000000..66f8e99 --- /dev/null +++ b/tests/statusdb/Makefile @@ -0,0 +1,2 @@ +SUBDIR=statusdb +include ../make/subdir.mk diff --git a/tests/statusdb/mixed.py b/tests/statusdb/mixed.py new file mode 100644 index 0000000..5daba53 --- /dev/null +++ b/tests/statusdb/mixed.py @@ -0,0 +1,59 @@ +import json +import sqlite3 +import sys + +def get_prop_type(prop: str): + prop = json.loads(prop or "[]") + name_parts = prop[-1].split("_") + if name_parts[0] == "\check": + # read_verilog style + # \check_cover_mixed_v... + return name_parts[1] + else: + # verific style + # \assert_auto_verificsva_cc... + return name_parts[0][1:] + +def main(): + workdir = sys.argv[1] + with open(f"{workdir}/status.path", "r") as status_path_file: + status_path = f"{workdir}/{status_path_file.read().rstrip()}" + # read only database + con = sqlite3.connect(f"file:{status_path}?mode=ro", uri=True) + db = con.cursor() + # custom sql to get all task property statuses for the current workdir + rows = db.execute( + """ + SELECT task.id, task_property.name, task_property.src, task_property_status.status + FROM task + LEFT JOIN task_property ON task_property.task=task.id + LEFT JOIN task_property_status ON task_property_status.task_property=task_property.id + WHERE task.workdir=:workdir; + """, + {"workdir": workdir} + ).fetchall() + # only check the most recent iteration of the test + last_id = 0 + for row_id, _, _, _ in rows: + if row_id > last_id: + last_id = row_id + for row_id, prop, src, status in rows: + if row_id != last_id: + continue + prop_type = get_prop_type(prop) + valid_status: list[None|str] = [] + if workdir in ["mixed_bmc", "mixed_assert"] and prop_type == "assert": + valid_status = ["FAIL"] + elif workdir == "mixed_bmc" and prop_type == "cover": + valid_status = [None, "UNKNOWN"] + elif workdir == "mixed_assert" and prop_type == "cover": + valid_status = ["PASS", None, "UNKNOWN"] + elif workdir == "mixed_no_assert" and prop_type == "assert": + valid_status = [None, "UNKNOWN"] + elif workdir == "mixed_no_assert" and prop_type == "cover": + valid_status = ["PASS"] + assert status in valid_status, f"Unexpected {prop_type} status {status} for {prop} ({src})" + + +if __name__ == "__main__": + main() diff --git a/tests/statusdb/mixed.sby b/tests/statusdb/mixed.sby new file mode 100644 index 0000000..7ad09c1 --- /dev/null +++ b/tests/statusdb/mixed.sby @@ -0,0 +1,24 @@ +[tasks] +no_assert cover +assert cover +bmc + +[options] +cover: mode cover +bmc: mode bmc +bmc: depth 1 + +assert: cover_assert on +no_assert: expect pass +~no_assert: expect fail + +[engines] +cover: smtbmc boolector +bmc: smtbmc boolector + +[script] +read -formal mixed.v +prep -top test + +[files] +mixed.v diff --git a/tests/statusdb/mixed.sh b/tests/statusdb/mixed.sh new file mode 100644 index 0000000..aca8be6 --- /dev/null +++ b/tests/statusdb/mixed.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 ${SBY_FILE%.sby}.py $WORKDIR diff --git a/tests/statusdb/mixed.v b/tests/statusdb/mixed.v new file mode 100644 index 0000000..16e1228 --- /dev/null +++ b/tests/statusdb/mixed.v @@ -0,0 +1,16 @@ +module test (input CP, CN, input A, B, output reg XP, XN); + reg [7:0] counter = 0; + always @* begin + assume (A || B); + assume (!A || !B); + assert (A == B); + cover (counter == 3 && A); + cover (counter == 3 && B); + end + always @(posedge CP) + counter <= counter + 1; + always @(posedge CP) + XP <= A; + always @(negedge CN) + XN <= B; +endmodule diff --git a/tests/unsorted/mixed.sby b/tests/unsorted/mixed.sby index 2d9467e..4948af0 100644 --- a/tests/unsorted/mixed.sby +++ b/tests/unsorted/mixed.sby @@ -8,6 +8,9 @@ cover: mode cover bmc: mode bmc bmc: depth 1 +cover: expect pass +~cover: expect fail + [engines] cover: btor btormc btormc: btor btormc diff --git a/tests/unsorted/mixed.v b/tests/unsorted/mixed.v index 26bf3c9..16e1228 100644 --- a/tests/unsorted/mixed.v +++ b/tests/unsorted/mixed.v @@ -3,7 +3,7 @@ module test (input CP, CN, input A, B, output reg XP, XN); always @* begin assume (A || B); assume (!A || !B); - assert (A != B); + assert (A == B); cover (counter == 3 && A); cover (counter == 3 && B); end