Merge pull request #330 from YosysHQ/krys/cover_no_assert

Remove asserts during cover mode

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

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

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)

tests/junit/junit_cover.sby

@@ -7,6 +7,7 @@ preunsat
 [options]
 mode cover
 depth 1
+cover_assert on
 
 pass: expect pass
 fail: expect fail

tests/statusdb/Makefile

@@ -0,0 +1,2 @@
+SUBDIR=statusdb
+include ../make/subdir.mk

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

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

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

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

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

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