mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-29 16:35:51 +00:00
Code Activity

Merge pull request #246 from YosysHQ/krys/scy_dev

Browse source 
Adding prep mode and skip_prep option
This commit is contained in:
Claire Xen 2023-07-18 16:46:40 +02:00 • committed by GitHub
commit cf0a761a3a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 30 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

54
sbysrc/sby_core.py
View file

@ -982,29 +982,30 @@ class SbyTask(SbyConfig):
with open(f"""{self.workdir}/model/design_prep.ys""", "w") as f:
print(f"# running in {self.workdir}/model/", file=f)
print(f"""read_ilang design.il""", file=f)
print("scc -select; simplemap; select -clear", file=f)
print("memory_nordff", file=f)
if self.opt_multiclock:
print("clk2fflogic", file=f)
else:
print("async2sync", file=f)
print("chformal -assume -early", file=f)
print("opt_clean", file=f)
print("formalff -setundef -clk2ff -ff2anyinit -hierarchy", file=f)
if self.opt_mode in ["bmc", "prove"]:
print("chformal -live -fair -cover -remove", file=f)
if self.opt_mode == "cover":
print("chformal -live -fair -remove", file=f)
if self.opt_mode == "live":
print("chformal -assert2assume", file=f)
print("chformal -cover -remove", file=f)
print("opt_clean", file=f)
print("check", file=f) # can't detect undriven wires past this point
print("setundef -undriven -anyseq", file=f)
print("opt -fast", file=f)
if self.opt_witrename:
print("rename -witness", file=f)
if not self.opt_skip_prep:
print("scc -select; simplemap; select -clear", file=f)
print("memory_nordff", file=f)
if self.opt_multiclock:
print("clk2fflogic", file=f)
else:
print("async2sync", file=f)
print("chformal -assume -early", file=f)
print("opt_clean", file=f)
print("formalff -setundef -clk2ff -ff2anyinit -hierarchy", file=f)
if self.opt_mode in ["bmc", "prove"]:
print("chformal -live -fair -cover -remove", file=f)
if self.opt_mode == "cover":
print("chformal -live -fair -remove", file=f)
if self.opt_mode == "live":
print("chformal -assert2assume", file=f)
print("chformal -cover -remove", file=f)
print("opt_clean", file=f)
print("check", file=f) # can't detect undriven wires past this point
print("setundef -undriven -anyseq", file=f)
print("opt -fast", file=f)
if self.opt_witrename:
print("rename -witness", file=f)
print("opt_clean", file=f)
print(f"""write_rtlil ../model/design_prep.il""", file=f)
proc = SbyProc(
@ -1212,7 +1213,7 @@ class SbyTask(SbyConfig):
self.handle_str_option("mode", None)
if self.opt_mode not in ["bmc", "prove", "cover", "live"]:
if self.opt_mode not in ["bmc", "prove", "cover", "live", "prep"]:
self.error(f"Invalid mode: {self.opt_mode}")
self.expect = ["PASS"]
@ -1249,6 +1250,7 @@ class SbyTask(SbyConfig):
self.handle_bool_option("append_assume", True)
self.handle_str_option("make_model", None)
self.handle_bool_option("skip_prep", False)
def setup_procs(self, setupmode):
self.handle_non_engine_options()
@ -1265,7 +1267,7 @@ class SbyTask(SbyConfig):
if engine[0] not in ["smtbmc", "btor"]:
self.error("Option skip is only valid for smtbmc and btor engines.")
if len(self.engine_list()) == 0:
if len(self.engine_list()) == 0 and self.opt_mode != "prep":
self.error("Config file is lacking engine configuration.")
if self.reusedir:
@ -1300,6 +1302,10 @@ class SbyTask(SbyConfig):
import sby_mode_cover
sby_mode_cover.run(self)
elif self.opt_mode == "prep":
self.model("prep")
self.update_status("PASS")
else:
assert False