From a332b017e4e3c74cc4a0bd442429ee0409775dd2 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 8 Jul 2025 15:47:31 +1200
Subject: [PATCH] More depth tracking

`SbyTask::update_status()` optionally takes the current step/depth, which gets used for some solvers/engines when exiting to pass unknown properties.
btor engine tracks the current step, but it doesn't track/report which property triggered a CEX so it's only useful on exit.
Use data source as a fallback if engine isn't provided (such as when coming from the `task_status` instead of an engine update).
---
 sbysrc/sby_core.py          | 7 +++++--
 sbysrc/sby_engine_btor.py   | 9 ++++++++-
 sbysrc/sby_engine_smtbmc.py | 7 ++++---
 sbysrc/sby_status.py        | 2 +-
 4 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 5ac0bc0..08334d4 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -1226,7 +1226,7 @@ class SbyTask(SbyConfig):
         for prop in self.design.pass_unknown_asserts():
             self.status_db.set_task_property_status(prop, data=data)
 
-    def update_status(self, new_status):
+    def update_status(self, new_status, step = None):
         assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
         self.status_db.set_task_status(new_status)
 
@@ -1240,7 +1240,10 @@ class SbyTask(SbyConfig):
             assert self.status != "FAIL"
             self.status = "PASS"
             if self.opt_mode in ("bmc", "prove") and self.design:
-                self.pass_unknown_asserts(dict(source="task_status"))
+                data = {"source": "task_status"}
+                if step:
+                    data["step"] = step
+                self.pass_unknown_asserts(data)
 
         elif new_status == "FAIL":
             assert self.status != "PASS"
diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py
index a3e744e..601f4f1 100644
--- a/sbysrc/sby_engine_btor.py
+++ b/sbysrc/sby_engine_btor.py
@@ -77,6 +77,7 @@ def run(mode, task, engine_idx, engine):
     common_state.wit_file = None
     common_state.assert_fail = False
     common_state.running_procs = 0
+    common_state.current_step = None
 
     def print_traces_and_terminate():
         if mode == "cover":
@@ -100,7 +101,7 @@ def run(mode, task, engine_idx, engine):
             else:
                 task.error(f"engine_{engine_idx}: Engine terminated without status.")
 
-        task.update_status(proc_status.upper())
+        task.update_status(proc_status.upper(), common_state.current_step)
         task.summary.set_engine_status(engine_idx, proc_status)
 
         task.terminate()
@@ -205,6 +206,9 @@ def run(mode, task, engine_idx, engine):
             if solver_args[0] == "btormc":
                 if "calling BMC on" in line:
                     return line
+                match = re.match(r".*at bound k = (\d+).*", line)
+                if match:
+                    common_state.current_step = int(match[1])
                 if "SATISFIABLE" in line:
                     return line
                 if "bad state properties at bound" in line:
@@ -215,6 +219,9 @@ def run(mode, task, engine_idx, engine):
                     return line
 
             elif solver_args[0] == "pono":
+                match = re.match(r".*at bound (\d+).*", line)
+                if match:
+                    common_state.current_step = int(match[1])
                 if line == "unknown":
                     if common_state.solver_status is None:
                         common_state.solver_status = "unsat"
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 0a3fdc4..34fdb8c 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -300,10 +300,11 @@ def run(mode, task, engine_idx, engine):
         simple_exit_callback(retcode)
 
     def last_exit_callback():
+        nonlocal current_step
         if mode == "bmc" or mode == "cover":
-            task.update_status(proc_status)
+            task.update_status(proc_status, current_step)
             if proc_status == "FAIL" and mode == "bmc" and keep_going:
-                task.pass_unknown_asserts(dict(source="smtbmc", keep_going=True, engine=f"engine_{engine_idx}"))
+                task.pass_unknown_asserts(dict(source="smtbmc", keep_going=True, engine=f"engine_{engine_idx}", step=current_step))
             proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status
             task.summary.set_engine_status(engine_idx, proc_status_lower)
             if not keep_going:
@@ -335,7 +336,7 @@ def run(mode, task, engine_idx, engine):
                 assert False
 
             if task.basecase_pass and task.induction_pass:
-                task.update_status("PASS")
+                task.update_status("PASS", current_step)
                 task.summary.append("successful proof by k-induction.")
                 if not keep_going:
                     task.terminate()
diff --git a/sbysrc/sby_status.py b/sbysrc/sby_status.py
index 3b07507..f153510 100644
--- a/sbysrc/sby_status.py
+++ b/sbysrc/sby_status.py
@@ -243,7 +243,7 @@ class SbyStatusDb:
                 round(now - self.start_time, 2),
                 self.task.name,
                 self.task.opt_mode,
-                data.get("engine", "ENGINE?"),
+                data.get("engine", data["source"]),
                 property.hdlname,
                 property.location,
                 property.status,