From 5014d740232c9a09ddea0f5f7d25dd3fe24de93f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 14 Jun 2022 18:04:24 +0200 Subject: [PATCH] sby_design: Extract total memory size and forall usage --- sbysrc/sby_core.py | 8 ++++---- sbysrc/sby_design.py | 26 +++++++++++++++++++++----- sbysrc/sby_engine_smtbmc.py | 10 +++++----- 3 files changed, 30 insertions(+), 14 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index d133786..cab8feb 100644 --- a/sbysrc/sby_core.py +++ b/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 diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index 8fc7895..399ea11 100644 --- a/sbysrc/sby_design.py +++ b/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"]) - return hierarchy + design.hierarchy = make_mod_hier(m["name"], m["name"]) + 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) - print("Design Hierarchy:", d) - for p in d.get_property_list(): + design = design_hierarchy(f) + print("Design Hierarchy:", design.hierarchy) + for p in design.hierarchy.get_property_list(): print("Property:", p) + print("Memory Bits:", design.memory_bits) if __name__ == '__main__': main() diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 0917763..8c11388 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/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") -- 2.30.2