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         mod = SbyModule(name=instance_name, type=module_name)
 107
 108         cells = design_json["modules"][module_name]["cells"]
 109         for cell_name, cell in cells.items():
 110             sub_hierarchy=f"{hierarchy}/{instance_name}" if hierarchy else instance_name
 111             if cell["type"][0] != '$' or cell["type"].startswith("$paramod"):
 112                 mod.submodules[cell_name] = make_mod_hier(cell_name, cell["type"], hierarchy=sub_hierarchy)
 113             if cell["type"] in ["$assume", "$assert", "$cover", "$live"]:
 114                 try:
 115                     location = cell["attributes"]["src"]
 116                 except KeyError:
 117                     location = ""
 118                 p = SbyProperty(name=cell_name, type=SbyProperty.Type.from_cell(cell["type"]), location=location, hierarchy=sub_hierarchy)
 119                 mod.properties.append(p)
 120         return mod
 121
 122     for module_name in design_json["modules"]:
 123         attrs = design_json["modules"][module_name]["attributes"]
 124         if "top" in attrs and int(attrs["top"]) == 1:
 125             hierarchy = make_mod_hier(module_name, module_name)
 126             return hierarchy
 127     else:
 128         raise ValueError("Cannot find top module")
 129
 130 def main():
 131     import sys
 132     if len(sys.argv) != 2:
 133         print(f"""Usage: {sys.argv[0]} design.json""")
 134     with open(sys.argv[1]) as f:
 135         d = design_hierarchy(f)
 136         print("Design Hierarchy:", d)
 137         for p in d.get_property_list():
 138             print("Property:", p)
 139
 140 if __name__ == '__main__':
 141     main()