mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-11-03 22:29:12 +00:00
Code Activity

assume_early option to implement cross assumes in IVY

Browse source 
Checking IVY's cross assumes requires delaying a subset of assumptions,
which we don't want SBY to undo.
This commit is contained in:
Jannis Harder 2023-08-11 15:58:55 +02:00
parent cf0a761a3a
commit 884ef862cb
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
sbysrc/sby_core.py
View file

@ -989,7 +989,8 @@ class SbyTask(SbyConfig):
print("clk2fflogic", file=f)
else:
print("async2sync", file=f)
print("chformal -assume -early", file=f)
if self.opt_assume_early:
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"]:
@ -1252,6 +1253,8 @@ class SbyTask(SbyConfig):
self.handle_str_option("make_model", None)
self.handle_bool_option("skip_prep", False)
self.handle_bool_option("assume_early", True)
def setup_procs(self, setupmode):
self.handle_non_engine_options()
if self.opt_smtc is not None: