mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-10-30 20:42:30 +00:00
Code Activity

Merge pull request #259 from jix/prepare-check

Browse source 
Prepare SBY for upcomming `$check` cell support and prevent backend failure for `$print` cells
This commit is contained in:
Jannis Harder 2024-01-23 10:05:02 +01:00 • committed by GitHub
commit bd9e218c4a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 29 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
sbysrc/sby_core.py
View file

@ -1055,6 +1055,7 @@ class SbyTask(SbyConfig):
print(f"# running in {self.workdir}/model/", file=f) print(f"# running in {self.workdir}/model/", file=f)
print(f"""read_ilang design_prep.il""", file=f) print(f"""read_ilang design_prep.il""", file=f)
print("hierarchy -smtcheck", file=f) print("hierarchy -smtcheck", file=f)
print("delete */t:$print", file=f)
print("formalff -assume", file=f) print("formalff -assume", file=f)
if "_nomem" in model_name: if "_nomem" in model_name:
print("memory_map -formal", file=f) print("memory_map -formal", file=f)
@ -1088,6 +1089,7 @@ class SbyTask(SbyConfig):
print(f"# running in {self.workdir}/model/", file=f) print(f"# running in {self.workdir}/model/", file=f)
print(f"""read_ilang design_prep.il""", file=f) print(f"""read_ilang design_prep.il""", file=f)
print("hierarchy -simcheck", file=f) print("hierarchy -simcheck", file=f)
print("delete */t:$print", file=f)
print("formalff -assume", file=f) print("formalff -assume", file=f)
if "_nomem" in model_name: if "_nomem" in model_name:
print("memory_map -formal", file=f) 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: with open(f"{self.workdir}/model/design_aiger.ys", "w") as f:
print(f"# running in {self.workdir}/model/", file=f) print(f"# running in {self.workdir}/model/", file=f)
print("read_ilang design_prep.il", file=f) print("read_ilang design_prep.il", file=f)
print("delete */t:$print", file=f)
print("hierarchy -simcheck", file=f) print("hierarchy -simcheck", file=f)
print("formalff -assume", file=f) print("formalff -assume", file=f)
print("flatten", file=f) print("flatten", file=f)

26
sbysrc/sby_design.py
View file

@ -71,6 +71,18 @@ class SbyProperty:
return c.LIVE return c.LIVE
raise ValueError("Unknown property type: " + name) 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 name: str
path: Tuple[str, ...] path: Tuple[str, ...]
type: Type type: Type
@ -199,6 +211,20 @@ def design_hierarchy(filename):
location=location, location=location,
hierarchy=sub_hierarchy) hierarchy=sub_hierarchy)
mod.properties.append(p) 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"): if sort["type"][0] != '$' or sort["type"].startswith("$paramod"):
for cell in sort["cells"]: for cell in sort["cells"]:
mod.submodules[cell["name"]] = make_mod_hier( mod.submodules[cell["name"]] = make_mod_hier(