From 53eb25fcaeddfdb7011ddba98c67f85b903fe8f0 Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Mon, 7 Feb 2022 15:29:36 +0100
Subject: [PATCH] handle unreached cover properties

---
 sbysrc/sby.py               |  2 +-
 sbysrc/sby_core.py          |  4 +++-
 sbysrc/sby_engine_smtbmc.py |  6 ++++++
 tests/cover_fail.sby        | 31 +++++++++++++++++++++++++++++++
 4 files changed, 41 insertions(+), 2 deletions(-)
 create mode 100644 tests/cover_fail.sby

diff --git a/sbysrc/sby.py b/sbysrc/sby.py
index 788c68b..5616bc0 100644
--- 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 9c7e3fd..8668b9d 100644
--- 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 e179dd5..a2553f2 100644
--- 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
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
-- 
2.30.2