From e9f4f06fe90a692777ea4ace2033dc177fdf7a45 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 8 Jul 2025 15:47:32 +1200
Subject: [PATCH] smtbmc updates db at each step

All properties marked UNKNOWN get dumped to the db for the previous step, each time the current step is updated.
---
 sbysrc/sby_core.py          | 5 +++++
 sbysrc/sby_engine_smtbmc.py | 3 +++
 2 files changed, 8 insertions(+)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 08334d4..033d42d 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -1222,6 +1222,11 @@ class SbyTask(SbyConfig):
         self.status = "ERROR"
         self.terminate()
 
+    def update_unknown_asserts(self, data):
+        for prop in self.design.hierarchy:
+            if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN":
+                self.status_db.set_task_property_status(prop, data=data)
+
     def pass_unknown_asserts(self, data):
         for prop in self.design.pass_unknown_asserts():
             self.status_db.set_task_property_status(prop, data=data)
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 34fdb8c..4deedf1 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -212,7 +212,10 @@ def run(mode, task, engine_idx, engine):
 
         match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line)
         if match:
+            last_step = current_step
             current_step = int(match[1])
+            if current_step != last_step and last_step is not None:
+                task.update_unknown_asserts(dict(source="smtbmc", engine=f"engine_{engine_idx}", step=last_step))
             return line
 
         match = re.match(r"^## [0-9: ]+ Status: FAILED", line)