From 3412ea859ba6510fda22aa3de140af78929f9d14 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Fri, 5 Aug 2022 15:51:11 +0200
Subject: [PATCH] New "none" engine to be used with the "make_model" option

---
 docs/source/reference.rst | 9 +++++++++
 sbysrc/sby_core.py        | 9 +++++----
 sbysrc/sby_mode_bmc.py    | 3 +++
 sbysrc/sby_mode_cover.py  | 3 +++
 sbysrc/sby_mode_live.py   | 3 +++
 sbysrc/sby_mode_prove.py  | 3 +++
 6 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 447673a..710ba7b 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -346,6 +346,15 @@ solvers:
 Solver options are passed as additional arguments to the ABC command
 implementing the solver.
 
+
+``none`` engine
+~~~~~~~~~~~~~~~
+
+The ``none`` engine does not run any solver. It can be used together with the
+``make_model`` option to manually generate any model supported by one of the
+other engines. This makes it easier to use the same models outside of sby.
+
+
 Script section
 --------------
 
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 2a1a994..7eab277 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -597,7 +597,8 @@ class SbyTask(SbyConfig):
                 else:
                     print("async2sync", file=f)
                     print("chformal -assume -early", file=f)
-                print("formalff -clk2ff -ff2anyinit", file=f)
+                print("opt_clean", file=f)
+                print("formalff -setundef -clk2ff -ff2anyinit", file=f)
                 if self.opt_mode in ["bmc", "prove"]:
                     print("chformal -live -fair -cover -remove", file=f)
                 if self.opt_mode == "cover":
@@ -661,7 +662,7 @@ class SbyTask(SbyConfig):
                 print("hierarchy -smtcheck", file=f)
                 if "_nomem" in model_name:
                     print("memory_map -formal", file=f)
-                    print("formalff -clk2ff -ff2anyinit", file=f)
+                    print("formalff -setundef -clk2ff -ff2anyinit", file=f)
                 if "_syn" in model_name:
                     print("techmap", file=f)
                     print("opt -fast", file=f)
@@ -693,7 +694,7 @@ class SbyTask(SbyConfig):
                 print("hierarchy -simcheck", file=f)
                 if "_nomem" in model_name:
                     print("memory_map -formal", file=f)
-                    print("formalff -clk2ff -ff2anyinit", file=f)
+                    print("formalff -setundef -clk2ff -ff2anyinit", file=f)
                 print("flatten", file=f)
                 print("setundef -undriven -anyseq", file=f)
                 if "_syn" in model_name:
@@ -726,7 +727,7 @@ class SbyTask(SbyConfig):
                 print("read_ilang design_prep.il", file=f)
                 print("hierarchy -simcheck", file=f)
                 print("memory_map -formal", file=f)
-                print("formalff -clk2ff -ff2anyinit", file=f)
+                print("formalff -setundef -clk2ff -ff2anyinit", file=f)
                 print("flatten", file=f)
                 print("setundef -undriven -anyseq", file=f)
                 print("setattr -unset keep", file=f)
diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index 78324ed..cc4eba7 100644
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -46,5 +46,8 @@ def run(task):
             import sby_engine_btor
             sby_engine_btor.run("bmc", task, engine_idx, engine)
 
+        elif engine[0] == "none":
+            pass
+
         else:
             task.error(f"Invalid engine '{engine[0]}' for bmc mode.")
diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py
index d7705ee..8fb1da9 100644
--- a/sbysrc/sby_mode_cover.py
+++ b/sbysrc/sby_mode_cover.py
@@ -37,5 +37,8 @@ def run(task):
             import sby_engine_btor
             sby_engine_btor.run("cover", task, engine_idx, engine)
 
+        elif engine[0] == "none":
+            pass
+
         else:
             task.error(f"Invalid engine '{engine[0]}' for cover mode.")
diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py
index 46b556f..6746200 100644
--- a/sbysrc/sby_mode_live.py
+++ b/sbysrc/sby_mode_live.py
@@ -34,5 +34,8 @@ def run(task):
             import sby_engine_aiger
             sby_engine_aiger.run("live", task, engine_idx, engine)
 
+        elif engine[0] == "none":
+            pass
+
         else:
             task.error(f"Invalid engine '{engine[0]}' for live mode.")
diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index 3abadf7..1f62bb9 100644
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -49,5 +49,8 @@ def run(task):
             import sby_engine_abc
             sby_engine_abc.run("prove", task, engine_idx, engine)
 
+        elif engine[0] == "none":
+            pass
+
         else:
             task.error(f"Invalid engine '{engine[0]}' for prove mode.")