create json export and read in properties

sbysrc/sby.py

@@ -455,18 +455,14 @@ def run_task(taskname):
 
     if not my_opt_tmpdir and not setupmode:
         with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f:
-            # TODO: create necessary data
+            checks = task.design_hierarchy.get_property_list()
-            # checks: collection of assert/cover statements active in task
-            # elements: dicts with entries 'type', 'hierarchy', 'location', 'status', 'tracefile'
-            checks = [ #for testing purposes
-            {'type':'assert', 'hierarchy':'top.dut.submod1', 'location':'test.v:404', 'status':'unknown', 'tracefile':'/home/user/path/task/engine_0/trace0.vcd'},
-            {'type':'assert', 'hierarchy':'top.dut.submod1', 'location':'test.v:412', 'status':'fail', 'tracefile':'/home/user/path/task/engine_0/trace1.vcd'},
-            {'type':'cover', 'hierarchy':'top.dut.submod2', 'location':'test3.v:42', 'status':'pass', 'tracefile':'/home/user/path/task/engine_1/trace0.vcd'},
-            {'type':'cover', 'hierarchy':'top.dut.submod2', 'location':'test3.v:666', 'status':'error', 'tracefile':'/home/user/path/task/engine_1/trace1.vcd'}
-            ]
             junit_tests = len(checks)
             junit_errors = 1 if task.retcode == 16 else 0
-            junit_failures = 1 if task.retcode != 0 and junit_errors == 0 else 0
+            junit_failures = 0
+            if task.retcode != 0 and junit_errors == 0:
+                for check in checks:
+                    if check.status == "FAIL":
+                        junit_failures += 1
             junit_type = "cover" if task.opt_mode == "cover" else "assert" #should this be here or individual for each check?
             junit_time = time.strftime('%Y-%m-%dT%H:%M:%S')
             print(f'<?xml version="1.0" encoding="UTF-8"?>', file=f)
@@ -478,12 +474,12 @@ def run_task(taskname):
             print(f'</properties>', file=f)
             for check in checks:
                 print(f'<testcase classname="{junit_tc_name}" name="" time="{task.total_time}">', file=f) # name required
-                if check["status"] == "unknown":
+                if check.status == "UNKNOWN":
                     print(f'<skipped />', file=f)
-                elif check["status"] == "fail":
+                elif check.status == "FAIL":
-                    print(f'<failure type="{check["type"]}" message="Property in {check["hierarchy"]} at {check["location"]} failed. Trace file: {check["tracefile"]}" />', file=f)
+                    print(f'<failure type="{check.type}" message="Property in {check.hierarchy} at {check.location} failed. Trace file: {check.tracefile}" />', file=f)
-                elif check["status"] == "error":
+                elif check.status == "ERROR":
-                    print(f'<error type="error"/>', file=f) # type mandatory, message optional
+                    print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
                 print(f'</testcase>', file=f)
             print('<system-out>', end="", file=f)
             with open(f"{task.workdir}/logfile.txt", "r") as logf:

sbysrc/sby_core.py

@@ -23,6 +23,7 @@ import subprocess
 from shutil import copyfile, copytree, rmtree
 from select import select
 from time import time, localtime, sleep
+from sby_design import SbyProperty, SbyModule, design_hierarchy
 
 all_procs_running = []
 
@@ -222,6 +223,7 @@ class SbyTask:
         self.status = "UNKNOWN"
         self.total_time = 0
         self.expect = []
+        self.design_hierarchy = None
 
         yosys_program_prefix = "" ##yosys-program-prefix##
         self.exe_paths = {
@@ -390,6 +392,8 @@ class SbyTask:
                 print("opt -keepdc -fast", file=f)
                 print("check", file=f)
                 print("hierarchy -simcheck", file=f)
+                # FIXME: can using design and design_nomem in the same task happen?
+                print(f"""write_json ../model/design{"" if model_name == "base" else "_nomem"}.json""", file=f)
                 print(f"""write_ilang ../model/design{"" if model_name == "base" else "_nomem"}.il""", file=f)
 
             proc = SbyProc(
@@ -401,6 +405,14 @@ class SbyTask:
             )
             proc.checkretcode = True
 
+            def instance_hierarchy_callback(retcode):
+                assert retcode == 0
+                assert self.design_hierarchy == None # verify this assumption
+                with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.json""") as f:
+                    self.design_hierarchy = design_hierarchy(f)
+
+            proc.exit_callback = instance_hierarchy_callback
+
             return [proc]
 
         if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name):

sbysrc/sby_design.py

@@ -0,0 +1,102 @@
+#
+# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
+#
+# Copyright (C) 2022  N. Engelhardt <nak@yosyshq.com>
+#
+# Permission to use, copy, modify, and/or distribute this software for any
+# purpose with or without fee is hereby granted, provided that the above
+# copyright notice and this permission notice appear in all copies.
+#
+# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+#
+
+import json
+from enum import Enum, auto
+from dataclasses import dataclass, field
+
+@dataclass
+class SbyProperty:
+    class Type(Enum):
+        ASSUME = auto()
+        ASSERT = auto()
+        COVER = auto()
+        LIVE = auto()
+
+        def __repr__(self):
+            return self.name
+
+        @classmethod
+        def from_cell(c, name):
+            if name == "$assume":
+                return c.ASSUME
+            if name == "$assert":
+                return c.ASSERT
+            if name == "$cover":
+                return c.COVER
+            if name == "$live":
+                return c.LIVE
+            raise ValueError("Unknown property type: " + name)
+
+    name: str
+    type: Type
+    location: str
+    hierarchy: str
+    status: str = field(default="UNKNOWN")
+    tracefile: str = field(default="")
+
+@dataclass
+class SbyModule:
+    name: str
+    type: str
+    submodules: dict = field(default_factory=dict)
+    properties: list = field(default_factory=list)
+
+    def get_property_list(self):
+        l = list()
+        l.extend(self.properties)
+        for submod in self.submodules:
+            l.extend(submod.get_property_list())
+        return l
+
+def design_hierarchy(filename):
+    design_json = json.load(filename)
+    def make_mod_hier(instance_name, module_name, hierarchy=""):
+        # print(instance_name,":", module_name)
+        mod = SbyModule(name=instance_name, type=module_name)
+
+        cells = design_json["modules"][module_name]["cells"]
+        for cell_name, cell in cells.items():
+            if cell["type"][0] != '$':
+                mod.submodules[cell_name] = make_mod_hier(cell_name, cell["type"], hierarchy=f"{hierarchy}/{instance_name}")
+            if cell["type"] in ["$assume", "$assert", "$cover", "$live"]:
+                try:
+                    location = cell["attributes"]["src"]
+                except KeyError:
+                    location = ""
+                p = SbyProperty(name=cell_name, type=SbyProperty.Type.from_cell(cell["type"]), location=location, hierarchy=f"{hierarchy}/{instance_name}")
+                mod.properties.append(p)
+        return mod
+
+    for module_name in design_json["modules"]:
+        attrs = design_json["modules"][module_name]["attributes"]
+        if "top" in attrs and int(attrs["top"]) == 1:
+            hierarchy = make_mod_hier(module_name, module_name)
+            return hierarchy
+    else:
+        raise ValueError("Cannot find top module")
+
+def main():
+    import sys
+    if len(sys.argv) != 2:
+        print(f"""Usage: {sys.argv[0]} design.json""")
+    with open(sys.argv[1]) as f:
+        print(design_hierarchy(f))
+
+if __name__ == '__main__':
+    main()