From acaf6ef0c2799e5ff506610bef23840c1f819853 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 16:34:25 +0200 Subject: [PATCH] Use new memory_map -formal for aiger/_nomem --- sbysrc/sby_core.py | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 8ef528d..08fd89f 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -661,7 +661,8 @@ class SbyTask(SbyConfig): print(f"""read_ilang design_prep.il""", file=f) print("hierarchy -smtcheck", file=f) if "_nomem" in model_name: - print("memory_map", file=f) + print("memory_map -formal", file=f) + print("formalff -clk2ff -ff2anyinit", file=f) if "_syn" in model_name: print("techmap", file=f) print("opt -fast", file=f) @@ -692,7 +693,8 @@ class SbyTask(SbyConfig): print(f"""read_ilang design_prep.il""", file=f) print("hierarchy -simcheck", file=f) if "_nomem" in model_name: - print("memory_map", file=f) + print("memory_map -formal", file=f) + print("formalff -clk2ff -ff2anyinit", file=f) print("flatten", file=f) print("setundef -undriven -anyseq", file=f) if "_syn" in model_name: @@ -724,7 +726,8 @@ class SbyTask(SbyConfig): print(f"# running in {self.workdir}/model/", file=f) print("read_ilang design_prep.il", file=f) print("hierarchy -simcheck", file=f) - print("memory_map", file=f) + print("memory_map -formal", file=f) + print("formalff -clk2ff -ff2anyinit", file=f) print("flatten", file=f) print("setundef -undriven -anyseq", file=f) print("setattr -unset keep", file=f)