More status tracking unification

- Status database only gets called from summary events instead of from engines.
- More trace witnesses (.aiw and .yw) are tracked as events.
- Multiple tracefiles can be included in the same trace summary, varying only by
  extension.  These are ordered by priority so that in the logfile only a single
  tracefile is listed.
- For engines where multiple properties can be collected for a single trace,
  these properties are now available for all traces until the next step.  If any
  properties are collected but never recorded with a trace, an error is raised.
- Fix formatting for events without steps (e.g. running abc with `vcd off`).
- Drop task_property_data table entirely, since it is now redundant and unused.
- Fix properties being skipped in all status dump if they don't have a trace.

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:

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)

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

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):

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)
 

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))