mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-08-15 09:25:31 +00:00
Code Activity

Initial live csv dumping

Browse source 
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).
This commit is contained in:
Krystine Sherwin 2025-07-08 15:47:31 +12:00
parent f63cd46d12
commit 0367db76f5
No known key found for this signature in database
3 changed files with 21 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby_engine_aiger.py
View file

@ -233,7 +233,7 @@ def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_v
cell_name = match[3] or match[2] cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
prop.status = "FAIL" 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) last_prop.append(prop)
return line return line

6
sbysrc/sby_engine_smtbmc.py
View file

@ -242,7 +242,7 @@ def run(mode, task, engine_idx, engine):
cell_name = match[3] or match[2] cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
prop.status = "FAIL" 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) last_prop.append(prop)
return line return line
@ -252,7 +252,7 @@ def run(mode, task, engine_idx, engine):
cell_name = match[3] or match[2] cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
prop.status = "PASS" 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) last_prop.append(prop)
return line return line
@ -284,7 +284,7 @@ def run(mode, task, engine_idx, engine):
cell_name = match[3] or match[2] cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
prop.status = "FAIL" 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 return line

20
sbysrc/sby_status.py
View file

@ -125,7 +125,8 @@ class SbyStatusDb:
self._setup() self._setup()
if task is not None: 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): def log_debug(self, *args):
if self.debug: if self.debug:
@ -148,13 +149,13 @@ class SbyStatusDb:
return schema_script != SQLSCRIPT return schema_script != SQLSCRIPT
@transaction @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( return self.db.execute(
""" """
INSERT INTO task (workdir, name, mode, created) INSERT INTO task (workdir, name, mode, created)
VALUES (:workdir, :name, :mode, :now) 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 ).lastrowid
@transaction @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 @transaction
def add_task_property_data(self, property: SbyProperty, kind: str, data: Any): def add_task_property_data(self, property: SbyProperty, kind: str, data: Any):
now = time.time() now = time.time()