diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index 02e853d..afcf5b3 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -233,7 +233,6 @@ 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}", step=current_step)) last_prop.append(prop) return line @@ -241,24 +240,30 @@ def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_v if match: tracefile = match[1] trace = os.path.basename(tracefile)[:-4] + trace_path = f"{task.workdir}/{tracefile}" task.summary.add_event(engine_idx=engine_idx, trace=trace, path=tracefile) + trace_id = task.status_db.add_task_trace(trace, trace_path) if match and last_prop: for p in last_prop: task.summary.add_event( engine_idx=engine_idx, trace=trace, type=p.celltype, hdlname=p.hdlname, src=p.location, step=current_step) - p.tracefiles.append(tracefile) + p.tracefiles.append(tracefile) + task.status_db.set_task_property_status(p, trace_id=trace_id, data=dict(source="aigsmt", engine=f"engine_{engine_idx}", step=current_step, trace_path=trace_path)) last_prop = [] return line return line def exit_callback2(retcode): + nonlocal last_prop if proc2_status is None: task.error(f"engine_{engine_idx}: Could not determine aigsmt status.") if proc2_status != "FAIL": task.error(f"engine_{engine_idx}: Unexpected aigsmt status.") + if len(last_prop): + task.error(f"engine_{engine_idx}: Found properties without trace.") proc2.output_callback = output_callback2 proc2.register_exit_callback(exit_callback2) diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 601f4f1..6f348e2 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -118,9 +118,12 @@ def run(mode, task, engine_idx, engine): def make_exit_callback(suffix): def exit_callback2(retcode): - vcdpath = f"engine_{engine_idx}/trace{suffix}.vcd" - if os.path.exists(f"{task.workdir}/{vcdpath}"): - task.summary.add_event(engine_idx=engine_idx, trace=f'trace{suffix}', path=vcdpath, type="$cover" if mode == "cover" else "$assert") + trace = f"trace{suffix}" + vcdpath = f"engine_{engine_idx}/{trace}.vcd" + trace_path = f"{task.workdir}/{vcdpath}" + if os.path.exists(trace_path): + task.summary.add_event(engine_idx=engine_idx, trace=trace, path=vcdpath, type="$cover" if mode == "cover" else "$assert") + task.status_db.add_task_trace(trace, trace_path) common_state.running_procs -= 1 if (common_state.running_procs == 0): diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 4deedf1..074f570 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -245,7 +245,6 @@ 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}", step=current_step)) last_prop.append(prop) return line @@ -255,7 +254,6 @@ 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}", step=current_step)) last_prop.append(prop) return line @@ -264,8 +262,10 @@ def run(mode, task, engine_idx, engine): if match: tracefile = match[1] trace = os.path.basename(tracefile)[:-4] + trace_path = f"{task.workdir}/{tracefile}" engine_case = mode.split('_')[1] if '_' in mode else None task.summary.add_event(engine_idx=engine_idx, trace=trace, path=tracefile, engine_case=engine_case) + trace_id = task.status_db.add_task_trace(trace, trace_path, engine_case) if match and last_prop: for p in last_prop: @@ -273,6 +273,7 @@ def run(mode, task, engine_idx, engine): engine_idx=engine_idx, trace=trace, type=p.celltype, hdlname=p.hdlname, src=p.location, step=current_step) p.tracefiles.append(tracefile) + task.status_db.set_task_property_status(p, trace_id=trace_id, data=dict(source="smtbmc", engine=f"engine_{engine_idx}", step=current_step, trace_path=trace_path)) last_prop = [] return line else: @@ -298,8 +299,11 @@ def run(mode, task, engine_idx, engine): last_exit_callback() def exit_callback(retcode): + nonlocal last_prop if proc_status is None: task.error(f"engine_{engine_idx}: Engine terminated without status.") + if len(last_prop): + task.error(f"engine_{engine_idx}: Found properties without trace.") simple_exit_callback(retcode) def last_exit_callback(): diff --git a/sbysrc/sby_status.py b/sbysrc/sby_status.py index bc6dc43..c356419 100644 --- a/sbysrc/sby_status.py +++ b/sbysrc/sby_status.py @@ -44,10 +44,12 @@ CREATE TABLE task_property ( CREATE TABLE task_property_status ( id INTEGER PRIMARY KEY, task_property INTEGER, + task_trace INTEGER, status TEXT, data TEXT, created REAL, - FOREIGN KEY(task_property) REFERENCES task_property(id) + FOREIGN KEY(task_property) REFERENCES task_property(id), + FOREIGN KEY(task_trace) REFERENCES task_trace(id) ); CREATE TABLE task_property_data ( id INTEGER PRIMARY KEY, @@ -56,6 +58,13 @@ CREATE TABLE task_property_data ( data TEXT, created REAL, FOREIGN KEY(task_property) REFERENCES task_property(id) +); +CREATE TABLE task_trace ( + id INTEGER PRIMARY KEY, + trace TEXT, + path TEXT, + engine_case TEXT, + created REAL );""" def transaction(method: Fn) -> Fn: @@ -219,6 +228,7 @@ class SbyStatusDb: self, property: SbyProperty, status: Optional[str] = None, + trace_id: Optional[int] = None, data: Any = None, ): if status is None: @@ -228,15 +238,16 @@ class SbyStatusDb: self.db.execute( """ INSERT INTO task_property_status ( - task_property, status, data, created + task_property, task_trace, status, data, created ) VALUES ( (SELECT id FROM task_property WHERE task = :task AND name = :name), - :status, :data, :now + :trace_id, :status, :data, :now ) """, dict( task=self.task_id, + trace_id=trace_id, name=json.dumps(property.path), status=status, data=json.dumps(data), @@ -254,6 +265,7 @@ class SbyStatusDb: property.location, property.kind, property.status, + data.get("trace_path", ""), data.get("step", ""), ] self.task.log(f"{click.style('csv', fg='yellow')}: {','.join(str(v) for v in csv)}") @@ -279,6 +291,26 @@ class SbyStatusDb: now=now, ), ) + + @transaction + def add_task_trace(self, trace: str, path: str, engine_case: Optional[str] = None): + now = time.time() + return self.db.execute( + """ + INSERT INTO task_trace ( + trace, path, engine_case, created + ) + VALUES ( + :trace, :path, :engine_case, :now + ) + """, + dict( + trace=trace, + path=path, + engine_case=engine_case, + now=now + ) + ).lastrowid def all_tasks(self): rows = self.db.execute( @@ -385,10 +417,11 @@ class SbyStatusDb: SELECT task.name as 'task_name', task.mode, task.created, task_property.kind, task_property.src as 'location', task_property.name, task_property.hdlname, task_property_status.status, task_property_status.data, task_property_status.created as 'status_created', - task_property_status.id + task_property_status.id, task_trace.path as 'trace_path' FROM task INNER JOIN task_property ON task_property.task=task.id - INNER JOIN task_property_status ON task_property_status.task_property=task_property.id; + INNER JOIN task_property_status ON task_property_status.task_property=task_property.id + INNER JOIN task_trace ON task_property_status.task_trace=task_trace.id; """ ).fetchall() @@ -414,6 +447,7 @@ class SbyStatusDb: "location", "kind", "status", + "trace", "depth", ] print(','.join(csv_header)) @@ -457,6 +491,7 @@ class SbyStatusDb: prop_status['location'], prop_status['kind'], status, + prop_status['trace_path'], depth, ] print(','.join("" if v is None else str(v) for v in csv_line))