From 0367db76f563612a98131fa507655f96b0d219ec 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] Initial live csv dumping Currently unconditional, and only for aiger and smtbmc. Uses task.name from intertask cancellation. Stores `time.time()` when calling `SbyStatusDb::create_task()` in order to calculate time since start of task (consider reducing to integer seconds). --- sbysrc/sby_engine_aiger.py | 2 +- sbysrc/sby_engine_smtbmc.py | 6 +++--- sbysrc/sby_status.py | 20 +++++++++++++++++--- 3 files changed, 21 insertions(+), 7 deletions(-) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 11e176f..02e853d 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -233,7 +233,7 @@ def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_v cell_name = match[3] or match[2] prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop.status = "FAIL" - task.status_db.set_task_property_status(prop, data=dict(source="aigsmt", engine=f"engine_{engine_idx}")) + task.status_db.set_task_property_status(prop, data=dict(source="aigsmt", engine=f"engine_{engine_idx}", step=current_step)) last_prop.append(prop) return line diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index fe0380e..0a3fdc4 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -242,7 +242,7 @@ def run(mode, task, engine_idx, engine): cell_name = match[3] or match[2] prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop.status = "FAIL" - task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}")) + task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}", step=current_step)) last_prop.append(prop) return line @@ -252,7 +252,7 @@ def run(mode, task, engine_idx, engine): cell_name = match[3] or match[2] prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop.status = "PASS" - task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}")) + task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}", step=current_step)) last_prop.append(prop) return line @@ -284,7 +284,7 @@ def run(mode, task, engine_idx, engine): cell_name = match[3] or match[2] prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop.status = "FAIL" - task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}")) + task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}", step=current_step)) return line diff --git a/sbysrc/sby_status.py b/sbysrc/sby_status.py index 12eb64f..3b07507 100644 --- a/sbysrc/sby_status.py +++ b/sbysrc/sby_status.py @@ -125,7 +125,8 @@ class SbyStatusDb: self._setup() if task is not None: - self.task_id = self.create_task(workdir=task.workdir, name=task.name, mode=task.opt_mode) + self.start_time = time.time() + self.task_id = self.create_task(workdir=task.workdir, name=task.name, mode=task.opt_mode, now=self.start_time) def log_debug(self, *args): if self.debug: @@ -148,13 +149,13 @@ class SbyStatusDb: return schema_script != SQLSCRIPT @transaction - def create_task(self, workdir: str, name: str, mode: str) -> int: + def create_task(self, workdir: str, name: str, mode: str, now:float) -> int: return self.db.execute( """ INSERT INTO task (workdir, name, mode, created) VALUES (:workdir, :name, :mode, :now) """, - dict(workdir=workdir, name=name, mode=mode, now=time.time()), + dict(workdir=workdir, name=name, mode=mode, now=now), ).lastrowid @transaction @@ -237,6 +238,19 @@ class SbyStatusDb: ), ) + if True: + csv = [ + round(now - self.start_time, 2), + self.task.name, + self.task.opt_mode, + data.get("engine", "ENGINE?"), + property.hdlname, + property.location, + property.status, + data.get("step", "DEPTH?"), + ] + self.task.log(f"csv: {','.join(str(v) for v in csv)}") + @transaction def add_task_property_data(self, property: SbyProperty, kind: str, data: Any): now = time.time()