diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 8d2fc76..d59ffa1 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1055,6 +1055,7 @@ class SbyTask(SbyConfig): print(f"# running in {self.workdir}/model/", file=f) print(f"""read_ilang design_prep.il""", file=f) print("hierarchy -smtcheck", file=f) + print("delete */t:$print", file=f) print("formalff -assume", file=f) if "_nomem" in model_name: print("memory_map -formal", file=f) @@ -1088,6 +1089,7 @@ class SbyTask(SbyConfig): print(f"# running in {self.workdir}/model/", file=f) print(f"""read_ilang design_prep.il""", file=f) print("hierarchy -simcheck", file=f) + print("delete */t:$print", file=f) print("formalff -assume", file=f) if "_nomem" in model_name: print("memory_map -formal", file=f) @@ -1122,6 +1124,7 @@ class SbyTask(SbyConfig): with open(f"{self.workdir}/model/design_aiger.ys", "w") as f: print(f"# running in {self.workdir}/model/", file=f) print("read_ilang design_prep.il", file=f) + print("delete */t:$print", file=f) print("hierarchy -simcheck", file=f) print("formalff -assume", file=f) print("flatten", file=f) diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index 88b6395..a449a9b 100644 --- a/sbysrc/sby_design.py +++ b/sbysrc/sby_design.py @@ -71,6 +71,18 @@ class SbyProperty: return c.LIVE raise ValueError("Unknown property type: " + name) + @classmethod + def from_flavor(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 path: Tuple[str, ...] type: Type @@ -199,6 +211,20 @@ def design_hierarchy(filename): location=location, hierarchy=sub_hierarchy) mod.properties.append(p) + if sort["type"] == "$check": + for cell in sort["cells"]: + try: + location = cell["attributes"]["src"] + except KeyError: + location = "" + p = SbyProperty( + name=cell["name"], + path=(*path, *cell_path(cell)), + type=SbyProperty.Type.from_flavor(cell["parameters"]["FLAVOR"]), + location=location, + hierarchy=sub_hierarchy) + mod.properties.append(p) + if sort["type"][0] != '$' or sort["type"].startswith("$paramod"): for cell in sort["cells"]: mod.submodules[cell["name"]] = make_mod_hier(