sbysrc/sby_design.py

   1 #
   2 # SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
   3 #
   4 # Copyright (C) 2022  N. Engelhardt <nak@yosyshq.com>
   5 #
   6 # Permission to use, copy, modify, and/or distribute this software for any
   7 # purpose with or without fee is hereby granted, provided that the above
   8 # copyright notice and this permission notice appear in all copies.
   9 #
  10 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17 #
  18
  19 import json
  20 from enum import Enum, auto
  21 from dataclasses import dataclass, field
  22
  23 @dataclass
  24 class SbyProperty:
  25     class Type(Enum):
  26         ASSUME = auto()
  27         ASSERT = auto()
  28         COVER = auto()
  29         LIVE = auto()
  30
  31         def __str__(self):
  32             return self.name
  33
  34         @classmethod
  35         def from_cell(c, name):
  36             if name == "$assume":
  37                 return c.ASSUME
  38             if name == "$assert":
  39                 return c.ASSERT
  40             if name == "$cover":
  41                 return c.COVER
  42             if name == "$live":
  43                 return c.LIVE
  44             raise ValueError("Unknown property type: " + name)
  45
  46     name: str
  47     type: Type
  48     location: str
  49     hierarchy: str
  50     status: str = field(default="UNKNOWN")
  51     tracefile: str = field(default="")
  52
  53     def __repr__(self):
  54         return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\">"
  55
  56 @dataclass
  57 class SbyModule:
  58     name: str
  59     type: str
  60     submodules: dict = field(default_factory=dict)
  61     properties: list = field(default_factory=list)
  62
  63     def __repr__(self):
  64         return f"SbyModule<{self.name} : {self.type}, submodules={self.submodules}, properties={self.properties}>"
  65
  66     def __iter__(self):
  67         for prop in self.properties:
  68             yield prop
  69         for submod in self.submodules.values():
  70             yield from submod.__iter__()
  71
  72     def get_property_list(self):
  73         return [p for p in self if p.type != p.Type.ASSUME]
  74
  75     def find_property(self, hierarchy, location):
  76         # FIXME: use that RE that works with escaped paths from https://stackoverflow.com/questions/46207665/regex-pattern-to-split-verilog-path-in-different-instances-using-python
  77         path = hierarchy.split('.')
  78         mod = path.pop(0)
  79         if self.name != mod:
  80             raise ValueError(f"{self.name} is not the first module in hierarchical path {hierarchy}.")
  81         try:
  82             mod_hier = self
  83             while path:
  84                 mod = path.pop(0)
  85                 mod_hier = mod_hier.submodules[mod]
  86         except KeyError:
  87             raise KeyError(f"Could not find {hierarchy} in design hierarchy!")
  88         try:
  89             prop = next(p for p in mod_hier.properties if location in p.location)
  90         except StopIteration:
  91             raise KeyError(f"Could not find assert at {location} in properties list!")
  92         return prop
  93
  94     def find_property_by_cellname(self, cell_name, trans_dict=dict()):
  95         # backends may need to mangle names irreversibly, so allow applying
  96         # the same transformation here
  97         for prop in self:
  98             if cell_name == prop.name.translate(str.maketrans(trans_dict)):
  99                 return prop
 100         raise KeyError(f"No such property: {cell_name}")
 101
 102 def design_hierarchy(filename):
 103     design_json = json.load(filename)
 104     def make_mod_hier(instance_name, module_name, hierarchy=""):
 105         # print(instance_name,":", module_name)
 106         sub_hierarchy=f"{hierarchy}/{instance_name}" if hierarchy else instance_name
 107         mod = SbyModule(name=instance_name, type=module_name)
 108
 109         for m in design_json["modules"]:
 110             if m["name"] == module_name:
 111                 cell_sorts = m["cell_sorts"]
 112                 break
 113         else:
 114             raise ValueError(f"Cannot find module {module_name}")
 115
 116         for sort in cell_sorts:
 117             if sort["type"] in ["$assume", "$assert", "$cover", "$live"]:
 118                 for cell in sort["cells"]:
 119                     try:
 120                         location = cell["attributes"]["src"]
 121                     except KeyError:
 122                         location = ""
 123                     p = SbyProperty(name=cell["name"], type=SbyProperty.Type.from_cell(sort["type"]), location=location, hierarchy=sub_hierarchy)
 124                     mod.properties.append(p)
 125             if sort["type"][0] != '$' or sort["type"].startswith("$paramod"):
 126                 for cell in sort["cells"]:
 127                     mod.submodules[cell["name"]] = make_mod_hier(cell["name"], sort["type"], hierarchy=sub_hierarchy)
 128         return mod
 129
 130     for m in design_json["modules"]:
 131         attrs = m["attributes"]
 132         if "top" in attrs and int(attrs["top"]) == 1:
 133             hierarchy = make_mod_hier(m["name"], m["name"])
 134             return hierarchy
 135     else:
 136         raise ValueError("Cannot find top module")
 137
 138 def main():
 139     import sys
 140     if len(sys.argv) != 2:
 141         print(f"""Usage: {sys.argv[0]} design.json""")
 142     with open(sys.argv[1]) as f:
 143         d = design_hierarchy(f)
 144         print("Design Hierarchy:", d)
 145         for p in d.get_property_list():
 146             print("Property:", p)
 147
 148 if __name__ == '__main__':
 149     main()