mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 14:04:07 +00:00
Code Activity

Enable yosys sim support for clock signals in hierarchical designs

Browse source
This commit is contained in:
Jannis Harder 2023-01-11 18:02:45 +01:00
parent 06c36d5bb0
commit 6398938e6a
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
sbysrc/sby_core.py
View file

@ -989,7 +989,7 @@ class SbyTask(SbyConfig):
print("async2sync", file=f) print("async2sync", file=f)
print("chformal -assume -early", file=f) print("chformal -assume -early", file=f)
print("opt_clean", file=f) print("opt_clean", file=f)
print("formalff -setundef -clk2ff -ff2anyinit", file=f) print("formalff -setundef -clk2ff -ff2anyinit -hierarchy", file=f)
if self.opt_mode in ["bmc", "prove"]: if self.opt_mode in ["bmc", "prove"]:
print("chformal -live -fair -cover -remove", file=f) print("chformal -live -fair -cover -remove", file=f)
if self.opt_mode == "cover": if self.opt_mode == "cover":
@ -1051,6 +1051,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("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)
print("formalff -setundef -clk2ff -ff2anyinit", file=f) print("formalff -setundef -clk2ff -ff2anyinit", file=f)
@ -1083,6 +1084,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("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)
print("formalff -setundef -clk2ff -ff2anyinit", file=f) print("formalff -setundef -clk2ff -ff2anyinit", file=f)
@ -1117,6 +1119,7 @@ class SbyTask(SbyConfig):
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("hierarchy -simcheck", file=f) print("hierarchy -simcheck", file=f)
print("formalff -assume", file=f)
print("flatten", file=f) print("flatten", file=f)
print("setundef -undriven -anyseq", file=f) print("setundef -undriven -anyseq", file=f)
print("setattr -unset keep", file=f) print("setattr -unset keep", file=f)

5
sbysrc/sby_sim.py
View file

@ -63,7 +63,10 @@ def sim_witness_trace(prefix, task, engine_idx, witness_file, *, append, deps=()
for assertion in summary["assertions"]: for assertion in summary["assertions"]:
if task.design: if task.design:
prop = task.design.properties_by_path[tuple(assertion["path"])] try:
prop = task.design.properties_by_path[tuple(assertion["path"])]
except KeyError:
prop = None
else: else:
prop = None prop = None