Skip to content

Commit

Permalink
assume_early option to implement cross assumes in IVY
Browse files Browse the repository at this point in the history
Checking IVY's cross assumes requires delaying a subset of assumptions,
which we don't want SBY to undo.
  • Loading branch information
jix committed Aug 11, 2023
1 parent cf0a761 commit 884ef86
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion sbysrc/sby_core.py
Original file line number Diff line number Diff line change
Expand Up @@ -989,7 +989,8 @@ def make_model(self, model_name):
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"]:
Expand Down Expand Up @@ -1252,6 +1253,8 @@ def handle_non_engine_options(self):
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:
Expand Down

0 comments on commit 884ef86

Please sign in to comment.