From 884ef862cbc0f34799cd6a6152f7dd384518d9bd Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 11 Aug 2023 15:58:55 +0200 Subject: [PATCH] assume_early option to implement cross assumes in IVY Checking IVY's cross assumes requires delaying a subset of assumptions, which we don't want SBY to undo. --- sbysrc/sby_core.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index ecd901ce..8d2fc764 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -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"]: @@ -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: