handle unreached cover properties

diff --git a/sbysrc/sby.py b/sbysrc/sby.py
index 788c68bf5f1fd15621d52a7fe005b8c119ac4558..5616bc0f0d76795d5449caeb55226fb956b98481 100644 (file)
--- a/sbysrc/sby.py
+++ b/sbysrc/sby.py
@@ -455,7 +455,7 @@ def run_task(taskname):
 
     if not my_opt_tmpdir and not setupmode:
         with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f:
-            task.print_junit_result(f, junit_ts_name, junit_tc_name)
+            task.print_junit_result(f, junit_ts_name, junit_tc_name, junit_format_strict=False)
 
         with open(f"{task.workdir}/status", "w") as f:
             print(f"{task.status} {task.retcode} {task.total_time}", file=f)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 9c7e3fd0198158ee16bdf89bc045c45a1bff7ef6..8668b9d081c01a5c58b00cff6fe6dcf6c236a852 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -756,6 +756,7 @@ class SbyTask:
             junit_failures = 0
         else:
             if self.precise_prop_status:
+                junit_failures = 0
                 for check in checks:
                     if check.status not in self.expect:
                         junit_failures += 1
@@ -777,7 +778,8 @@ class SbyTask:
                 elif check.status == "UNKNOWN":
                     print(f'<skipped />', file=f)
                 elif check.status == "FAIL":
-                    print(f'<failure type="{check.type}" message="Property in {check.hierarchy} at {check.location} failed. Trace file: {check.tracefile}" />', file=f)
+                    traceinfo = f' Trace file: {check.tracefile}' if check.type == check.Type.ASSERT else ''
+                    print(f'<failure type="{check.type}" message="Property {check.type} in {check.hierarchy} at {check.location} failed.{traceinfo}" />', file=f)
                 elif check.status == "ERROR":
                     print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
                 print(f'</testcase>', file=f)

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index e179dd54fe175c24946cbd365991491872353550..a2553f220714fd9fce2b4b3974f661bf12c49f43 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -201,6 +201,12 @@ def run(mode, task, engine_idx, engine):
             last_prop.tracefile = match[1]
             last_prop = None
 
+        match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line)
+        if match:
+            cell_name = match[2]
+            prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+            prop.status = "FAIL"
+
         return line
 
     def exit_callback(retcode):

diff --git a/tests/cover_fail.sby b/tests/cover_fail.sby
new file mode 100644 (file)
index 0000000..f169a5f
--- /dev/null
+++ b/tests/cover_fail.sby
@@ -0,0 +1,31 @@
+[options]
+mode cover
+depth 5
+expect fail
+
+[engines]
+smtbmc boolector
+
+[script]
+read_verilog -sv test.v
+prep -top test
+
+[file test.v]
+module test(
+input clk,
+input rst,
+output reg [3:0] count
+);
+
+initial assume (rst == 1'b1);
+
+always @(posedge clk) begin
+if (rst)
+  count <= 4'b0;
+else
+  count <= count + 1'b1;
+
+cover (count == 0);
+cover (count == 4'd11);
+end
+endmodule