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

New "none" engine to be used with the "make_model" option

Browse source
This commit is contained in:
Jannis Harder 2022-08-05 15:51:11 +02:00
parent 231f0b80aa
commit 3412ea859b
6 changed files with 26 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
sbysrc/sby_core.py
View file

@ -597,7 +597,8 @@ class SbyTask(SbyConfig):
else:
print("async2sync", file=f)
print("chformal -assume -early", file=f)
print("formalff -clk2ff -ff2anyinit", file=f)
print("opt_clean", file=f)
print("formalff -setundef -clk2ff -ff2anyinit", file=f)
if self.opt_mode in ["bmc", "prove"]:
print("chformal -live -fair -cover -remove", file=f)
if self.opt_mode == "cover":
@ -661,7 +662,7 @@ class SbyTask(SbyConfig):
print("hierarchy -smtcheck", file=f)
if "_nomem" in model_name:
print("memory_map -formal", file=f)
print("formalff -clk2ff -ff2anyinit", file=f)
print("formalff -setundef -clk2ff -ff2anyinit", file=f)
if "_syn" in model_name:
print("techmap", file=f)
print("opt -fast", file=f)
@ -693,7 +694,7 @@ class SbyTask(SbyConfig):
print("hierarchy -simcheck", file=f)
if "_nomem" in model_name:
print("memory_map -formal", file=f)
print("formalff -clk2ff -ff2anyinit", file=f)
print("formalff -setundef -clk2ff -ff2anyinit", file=f)
print("flatten", file=f)
print("setundef -undriven -anyseq", file=f)
if "_syn" in model_name:
@ -726,7 +727,7 @@ class SbyTask(SbyConfig):
print("read_ilang design_prep.il", file=f)
print("hierarchy -simcheck", file=f)
print("memory_map -formal", file=f)
print("formalff -clk2ff -ff2anyinit", file=f)
print("formalff -setundef -clk2ff -ff2anyinit", file=f)
print("flatten", file=f)
print("setundef -undriven -anyseq", file=f)
print("setattr -unset keep", file=f)

3
sbysrc/sby_mode_bmc.py
View file

@ -46,5 +46,8 @@ def run(task):
import sby_engine_btor
sby_engine_btor.run("bmc", task, engine_idx, engine)
elif engine[0] == "none":
pass
else:
task.error(f"Invalid engine '{engine[0]}' for bmc mode.")

3
sbysrc/sby_mode_cover.py
View file

@ -37,5 +37,8 @@ def run(task):
import sby_engine_btor
sby_engine_btor.run("cover", task, engine_idx, engine)
elif engine[0] == "none":
pass
else:
task.error(f"Invalid engine '{engine[0]}' for cover mode.")

3
sbysrc/sby_mode_live.py
View file

@ -34,5 +34,8 @@ def run(task):
import sby_engine_aiger
sby_engine_aiger.run("live", task, engine_idx, engine)
elif engine[0] == "none":
pass
else:
task.error(f"Invalid engine '{engine[0]}' for live mode.")

3
sbysrc/sby_mode_prove.py
View file

@ -49,5 +49,8 @@ def run(task):
import sby_engine_abc
sby_engine_abc.run("prove", task, engine_idx, engine)
elif engine[0] == "none":
pass
else:
task.error(f"Invalid engine '{engine[0]}' for prove mode.")