diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 2528ab6..e97c6aa 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -20,6 +20,7 @@ import os, re, sys, signal, platform, click if os.name == "posix": import resource, fcntl import subprocess +from pathlib import Path from dataclasses import dataclass, field from collections import defaultdict from typing import Optional @@ -631,6 +632,8 @@ class SbyTraceSummary: path: Optional[str] = field(default=None) engine_case: Optional[str] = field(default=None) events: dict = field(default_factory=lambda: defaultdict(lambda: defaultdict(list))) + trace_ids: dict[str, int] = field(default_factory=lambda: dict()) + last_ext: Optional[str] = field(default=None) @property def kind(self): @@ -682,42 +685,68 @@ class SbySummary: if update_status: status_metadata = dict(source="summary_event", engine=engine.engine) + if event.step: + status_metadata["step"] = event.step if event.prop: - if event.type == "$assert": + add_trace = False + if event.type is None: + event.type = event.prop.celltype + elif event.type == "$assert": event.prop.status = "FAIL" - if event.path: - event.prop.tracefiles.append(event.path) - if update_status: - self.task.status_db.add_task_property_data( - event.prop, - "trace", - data=dict(path=event.path, step=event.step, **status_metadata), - ) - if event.prop: - if event.type == "$cover": + add_trace = True + elif event.type == "$cover": event.prop.status = "PASS" - if event.path: - event.prop.tracefiles.append(event.path) - if update_status: - self.task.status_db.add_task_property_data( - event.prop, - "trace", - data=dict(path=event.path, step=event.step, **status_metadata), - ) + add_trace = True + + if event.path and add_trace: + event.prop.tracefiles.append(event.path) + + trace_path = None + if event.trace: + # get or create trace summary + try: + trace_summary = engine.traces[event.trace] + except KeyError: + trace_summary = SbyTraceSummary(event.trace, path=event.path, engine_case=event.engine_case) + engine.traces[event.trace] = trace_summary + + if event.path: + trace_path = Path(event.path) + trace_ext = trace_path.suffix + trace_summary.last_ext = trace_ext + try: + # use existing tracefile for this extension + trace_id = trace_summary.trace_ids[trace_ext] + except KeyError: + # add tracefile to database + trace_id = self.task.status_db.add_task_trace(event.trace, event.path, trace_ext[1:], event.engine_case) + trace_summary.trace_ids[trace_ext] = trace_id + elif trace_summary.path: + # use existing tracefile for last extension + trace_path = Path(trace_summary.path) + trace_ext = trace_summary.last_ext + trace_id = trace_summary.trace_ids[trace_ext] + + if event.type: + by_type = trace_summary.events[event.type] + if event.hdlname: + by_type[event.hdlname].append(event) + if event.prop and update_status: - self.task.status_db.set_task_property_status( - event.prop, - data=status_metadata - ) - - if event.trace not in engine.traces: - engine.traces[event.trace] = SbyTraceSummary(event.trace, path=event.path, engine_case=event.engine_case) - - if event.type: - by_type = engine.traces[event.trace].events[event.type] - if event.hdlname: - by_type[event.hdlname].append(event) + # update property status in database + if trace_path: + self.task.status_db.set_task_property_status( + event.prop, + trace_id=trace_id, + trace_path=Path(self.task.workdir, trace_path).with_suffix(trace_ext), + data=status_metadata, + ) + else: + self.task.status_db.set_task_property_status( + event.prop, + data=status_metadata, + ) def set_engine_status(self, engine_idx, status, case=None): engine_summary = self.engine_summary(engine_idx) @@ -759,10 +788,21 @@ class SbySummary: break case_suffix = f" [{trace.engine_case}]" if trace.engine_case else "" if trace.path: - if short: - yield f"{trace.kind}{case_suffix}: {self.task.workdir}/{trace.path}" - else: - yield f"{trace.kind}{case_suffix}: {trace.path}" + # print single preferred trace + preferred_exts = [".fst", ".vcd"] + if trace.last_ext not in preferred_exts: preferred_exts.append(trace.last_ext) + for ext in trace.trace_ids.keys(): + if ext not in preferred_exts: preferred_exts.append(ext) + for ext in preferred_exts: + if ext not in trace.trace_ids: + continue + if short: + path = Path(self.task.workdir) / trace.path + else: + path = Path(trace.path) + yield f"{trace.kind}{case_suffix}: {path.with_suffix(ext)}" + if short: + break else: yield f"{trace.kind}{case_suffix}: <{trace.trace}>" produced_traces = True @@ -785,15 +825,18 @@ class SbySummary: break event = same_events[0] - steps = sorted(e.step for e in same_events) + # uniquify steps and ignore events with missing steps + steps = sorted(set(e.step for e in same_events if e.step)) if short and len(steps) > step_limit: excess = len(steps) - step_limit steps = [str(step) for step in steps[:step_limit]] omitted_excess = True steps[-1] += f" and {excess} further step{'s' if excess != 1 else ''}" - steps = f"step{'s' if len(steps) > 1 else ''} {', '.join(map(str, steps))}" - yield f" {desc} {event.hdlname} at {event.src} in {steps}" + event_string = f" {desc} {hdlname} at {event.src}" + if steps: + event_string += f" step{'s' if len(steps) > 1 else ''} {', '.join(map(str, steps))}" + yield event_string if not produced_traces: yield f"{engine.engine} did not produce any traces" @@ -801,7 +844,7 @@ class SbySummary: if self.unreached_covers is None and self.task.opt_mode == 'cover' and self.task.status != "PASS" and self.task.design: self.unreached_covers = [] for prop in self.task.design.hierarchy: - if prop.type == prop.Type.COVER and prop.status == "UNKNOWN": + if prop.type == prop.Type.COVER and prop.status in ["UNKNOWN", "FAIL"]: self.unreached_covers.append(prop) if self.unreached_covers: diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 3527035..d8e0189 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -18,6 +18,7 @@ import re, getopt import json +import os from sby_core import SbyProc from sby_engine_aiger import aigsmt_exit_callback, aigsmt_trace_callback @@ -173,18 +174,25 @@ def run(mode, task, engine_idx, engine): aiger_props.append(task.design.properties_by_path.get(tuple(path))) if keep_going: - match = re.match(r"Writing CEX for output ([0-9]+) to engine_[0-9]+/(.*)\.aiw", line) + match = re.match(r"Writing CEX for output ([0-9]+) to (engine_[0-9]+/(.*)\.aiw)", line) if match: output = int(match[1]) + tracefile = match[2] + name = match[3] + trace, _ = os.path.splitext(name) + task.summary.add_event(engine_idx=engine_idx, trace=trace, path=tracefile) prop = aiger_props[output] if prop: prop.status = "FAIL" - task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) + task.summary.add_event( + engine_idx=engine_idx, trace=trace, + hdlname=prop.hdlname, src=prop.location, prop=prop, + ) disproved.add(output) proc_status = "FAIL" proc = aigsmt_trace_callback(task, engine_idx, proc_status, run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append, - name=match[2], + name=name, ) proc.register_exit_callback(exit_callback) procs_running += 1 @@ -198,7 +206,10 @@ def run(mode, task, engine_idx, engine): prop = aiger_props[output] if prop: prop.status = "PASS" - task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) + task.summary.add_event( + engine_idx=engine_idx, trace=None, + hdlname=prop.hdlname, src=prop.location, prop=prop, + ) proved.add(output) match = re.match(r"^Simulation of [0-9]+ frames for [0-9]+ rounds with [0-9]+ restarts did not assert POs.", line) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index afcf5b3..72add92 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -202,11 +202,13 @@ def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_v proc2_status = None last_prop = [] + recorded_last = False current_step = None def output_callback2(line): nonlocal proc2_status nonlocal last_prop + nonlocal recorded_last nonlocal current_step smt2_trans = {'\\':'/', '|':'/'} @@ -218,6 +220,8 @@ def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_v match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line) if match: + last_prop = [] + recorded_last = False current_step = int(match[1]) return line @@ -236,33 +240,29 @@ def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_v last_prop.append(prop) return line - match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line) + match = re.match(r"^## [0-9: ]+ Writing trace to (VCD|Yosys witness) file: (\S+)", line) if match: - tracefile = match[1] - trace = os.path.basename(tracefile)[:-4] - trace_path = f"{task.workdir}/{tracefile}" + tracefile = match[2] + trace, _ = os.path.splitext(os.path.basename(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) - 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 = [] + type=p.celltype, hdlname=p.hdlname, src=p.location, + step=current_step, prop=p, + ) + recorded_last = True return line return line def exit_callback2(retcode): - nonlocal last_prop + nonlocal last_prop, recorded_last 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): + if len(last_prop) and not recorded_last: task.error(f"engine_{engine_idx}: Found properties without trace.") proc2.output_callback = output_callback2 diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 6f348e2..9ef947e 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -123,7 +123,6 @@ def run(mode, task, engine_idx, engine): 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 074f570..52f0459 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -184,6 +184,7 @@ def run(mode, task, engine_idx, engine): proc_status = None last_prop = [] + recorded_last = False pending_sim = None current_step = None procs_running = 1 @@ -192,6 +193,7 @@ def run(mode, task, engine_idx, engine): def output_callback(line): nonlocal proc_status nonlocal last_prop + nonlocal recorded_last nonlocal pending_sim nonlocal current_step nonlocal procs_running @@ -212,6 +214,8 @@ def run(mode, task, engine_idx, engine): match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line) if match: + last_prop = [] + recorded_last = False last_step = current_step current_step = int(match[1]) if current_step != last_step and last_step is not None: @@ -257,30 +261,22 @@ def run(mode, task, engine_idx, engine): last_prop.append(prop) return line - if smtbmc_vcd and not task.opt_fst: - match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line) - 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: - 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) - 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: - match = re.match(r"^## [0-9: ]+ Writing trace to Yosys witness file: (\S+)", line) - if match: - tracefile = match[1] + match = re.match(r"^## [0-9: ]+ Writing trace to (VCD|Yosys witness) file: (\S+)", line) + if match: + tracefile = match[2] + if match[1] == "Yosys witness" and (task.opt_fst or task.opt_vcd_sim): pending_sim = tracefile + trace, _ = os.path.splitext(os.path.basename(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) + 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, prop=p, + ) + recorded_last = True + return line match = re.match(r"^## [0-9: ]+ Unreached cover statement at ([^:]+): (\S+)(?: \((\S+)\))?", line) if match and not failed_assert: @@ -288,7 +284,11 @@ 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)) + task.summary.add_event( + engine_idx=engine_idx, trace=None, + hdlname=prop.hdlname, src=prop.location, + step=current_step, prop=prop, + ) return line @@ -299,10 +299,10 @@ def run(mode, task, engine_idx, engine): last_exit_callback() def exit_callback(retcode): - nonlocal last_prop + nonlocal last_prop, recorded_last if proc_status is None: task.error(f"engine_{engine_idx}: Engine terminated without status.") - if len(last_prop): + if len(last_prop) and not recorded_last: task.error(f"engine_{engine_idx}: Found properties without trace.") simple_exit_callback(retcode) diff --git a/sbysrc/sby_status.py b/sbysrc/sby_status.py index c356419..50ed71a 100644 --- a/sbysrc/sby_status.py +++ b/sbysrc/sby_status.py @@ -51,20 +51,15 @@ CREATE TABLE task_property_status ( 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, - task_property INTEGER, - kind TEXT, - data TEXT, - created REAL, - FOREIGN KEY(task_property) REFERENCES task_property(id) -); CREATE TABLE task_trace ( id INTEGER PRIMARY KEY, + task INTEGER, trace TEXT, path TEXT, + kind TEXT, engine_case TEXT, - created REAL + created REAL, + FOREIGN KEY(task) REFERENCES task(id) );""" def transaction(method: Fn) -> Fn: @@ -229,6 +224,7 @@ class SbyStatusDb: property: SbyProperty, status: Optional[str] = None, trace_id: Optional[int] = None, + trace_path: str = "", data: Any = None, ): if status is None: @@ -265,49 +261,38 @@ class SbyStatusDb: property.location, property.kind, property.status, - data.get("trace_path", ""), + trace_path, data.get("step", ""), ] self.task.log(f"{click.style('csv', fg='yellow')}: {','.join(str(v) for v in csv)}") - - @transaction - def add_task_property_data(self, property: SbyProperty, kind: str, data: Any): - now = time.time() - self.db.execute( - """ - INSERT INTO task_property_data ( - task_property, kind, data, created - ) - VALUES ( - (SELECT id FROM task_property WHERE task = :task AND name = :name), - :kind, :data, :now - ) - """, - dict( - task=self.task_id, - name=json.dumps(property.path), - kind=kind, - data=json.dumps(data), - now=now, - ), - ) @transaction - def add_task_trace(self, trace: str, path: str, engine_case: Optional[str] = None): + def add_task_trace( + self, + trace: str, + path: str, + kind: str, + engine_case: Optional[str] = None, + task_id: Optional[int] = None, + ): + if task_id is None: + task_id = self.task_id now = time.time() return self.db.execute( """ INSERT INTO task_trace ( - trace, path, engine_case, created + trace, task, path, engine_case, kind, created ) VALUES ( - :trace, :path, :engine_case, :now + :trace, :task, :path, :engine_case, :kind, :now ) """, dict( trace=trace, + task=task_id, path=path, engine_case=engine_case, + kind=kind, now=now ) ).lastrowid @@ -414,14 +399,14 @@ class SbyStatusDb: def all_status_data_joined(self): rows = self.db.execute( """ - SELECT task.name as 'task_name', task.mode, task.created, task_property.kind, + SELECT task.name as 'task_name', task.mode, task.workdir, 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_trace.path as 'trace_path' + task_property_status.id, task_trace.path as '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_trace ON task_property_status.task_trace=task_trace.id; + LEFT JOIN task_trace ON task_property_status.task_trace=task_trace.id; """ ).fetchall() @@ -480,6 +465,10 @@ class SbyStatusDb: engine = prop_status['data'].get('engine', prop_status['data']['source']) time = prop_status['status_created'] - prop_status['created'] name = prop_status['hdlname'] + try: + trace_path = f"{prop_status['workdir']}/{prop_status['path']}" + except KeyError: + trace_path = None # print as csv csv_line = [ @@ -491,7 +480,7 @@ class SbyStatusDb: prop_status['location'], prop_status['kind'], status, - prop_status['trace_path'], + trace_path, depth, ] print(','.join("" if v is None else str(v) for v in csv_line))