sby_design: Extract total memory size and forall usage

sbysrc/sby_core.py

@@ -385,7 +385,7 @@ class SbyTask(SbyConfig):
         self.status = "UNKNOWN"
         self.total_time = 0
         self.expect = list()
-        self.design_hierarchy = None
+        self.design = None
         self.precise_prop_status = False
         self.timeout_reached = False
         self.task_local_abort = False
@@ -572,9 +572,9 @@ class SbyTask(SbyConfig):
             proc.checkretcode = True
 
             def instance_hierarchy_callback(retcode):
-                if self.design_hierarchy == None:
+                if self.design == None:
                     with open(f"{self.workdir}/model/design.json") as f:
-                        self.design_hierarchy = design_hierarchy(f)
+                        self.design = design_hierarchy(f)
 
             def instance_hierarchy_error_callback(retcode):
                 self.precise_prop_status = False
@@ -848,7 +848,7 @@ class SbyTask(SbyConfig):
     def print_junit_result(self, f, junit_ts_name, junit_tc_name, junit_format_strict=False):
         junit_time = strftime('%Y-%m-%dT%H:%M:%S')
         if self.precise_prop_status:
-            checks = self.design_hierarchy.get_property_list()
+            checks = self.design.hierarchy.get_property_list()
             junit_tests = len(checks)
             junit_failures = 0
             junit_errors = 0

sbysrc/sby_design.py

@@ -99,7 +99,16 @@ class SbyModule:
                 return prop
         raise KeyError(f"No such property: {cell_name}")
 
+
+@dataclass
+class SbyDesign:
+    hierarchy: SbyModule = None
+    memory_bits: int = 0
+    forall: bool = False
+
+
 def design_hierarchy(filename):
+    design = SbyDesign(hierarchy=None)
     design_json = json.load(filename)
     def make_mod_hier(instance_name, module_name, hierarchy=""):
         # print(instance_name,":", module_name)
@@ -125,13 +134,19 @@ def design_hierarchy(filename):
             if sort["type"][0] != '$' or sort["type"].startswith("$paramod"):
                 for cell in sort["cells"]:
                     mod.submodules[cell["name"]] = make_mod_hier(cell["name"], sort["type"], hierarchy=sub_hierarchy)
+            if sort["type"] in ["$mem", "$mem_v2"]:
+                for cell in sort["cells"]:
+                    design.memory_bits += int(cell["parameters"]["WIDTH"], 2) * int(cell["parameters"]["SIZE"], 2)
+            if sort["type"] in ["$allconst", "$allseq"]:
+                design.forall = True
+
         return mod
 
     for m in design_json["modules"]:
         attrs = m["attributes"]
         if "top" in attrs and int(attrs["top"]) == 1:
-            hierarchy = make_mod_hier(m["name"], m["name"])
+            design.hierarchy = make_mod_hier(m["name"], m["name"])
-            return hierarchy
+            return design
     else:
         raise ValueError("Cannot find top module")
 
@@ -140,10 +155,11 @@ def main():
     if len(sys.argv) != 2:
         print(f"""Usage: {sys.argv[0]} design.json""")
     with open(sys.argv[1]) as f:
-        d = design_hierarchy(f)
+        design = design_hierarchy(f)
-        print("Design Hierarchy:", d)
+        print("Design Hierarchy:", design.hierarchy)
-        for p in d.get_property_list():
+        for p in design.hierarchy.get_property_list():
             print("Property:", p)
+        print("Memory Bits:", design.memory_bits)
 
 if __name__ == '__main__':
     main()

sbysrc/sby_engine_smtbmc.py

@@ -194,7 +194,7 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line)
         if match:
             cell_name = match[3]
-            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
+            prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
             last_prop.append(prop)
             return line
@@ -202,7 +202,7 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line)
         if match:
             cell_name = match[2]
-            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
+            prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "PASS"
             last_prop.append(prop)
             return line
@@ -218,7 +218,7 @@ def run(mode, task, engine_idx, engine):
         match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line)
         if match:
             cell_name = match[2]
-            prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
+            prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
 
         return line
@@ -250,7 +250,7 @@ def run(mode, task, engine_idx, engine):
                     if excess_traces > 0:
                         task.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""")
             elif proc_status == "PASS" and mode == "bmc":
-                for prop in task.design_hierarchy:
+                for prop in task.design.hierarchy:
                     if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN":
                         prop.status = "PASS"
 
@@ -285,7 +285,7 @@ def run(mode, task, engine_idx, engine):
                 assert False
 
             if task.basecase_pass and task.induction_pass:
-                for prop in task.design_hierarchy:
+                for prop in task.design.hierarchy:
                     if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN":
                         prop.status = "PASS"
                 task.update_status("PASS")