diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 8d00314..710ba7b 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -153,6 +153,12 @@ options are:
 | ``tbtop``        |   All      | The top module for generated Verilog test benches, as   |
 |                  |            | hierarchical path relative to the design top module.    |
 +------------------+------------+---------------------------------------------------------+
+| ``make_model``   |   All      | Force generation of the named formal models. Takes a    |
+|                  |            | comma-separated list of model names. For a model        |
+|                  |            | ``<name>`` this will generate the                       |
+|                  |            | ``model/design_<name>.*`` files within the working      |
+|                  |            | directory, even when not required to run the task.      |
++------------------+------------+---------------------------------------------------------+
 | ``smtc``         | ``bmc``,   | Pass this ``.smtc`` file to the smtbmc engine. All      |
 |                  | ``prove``, | other engines are disabled when this option is used.    |
 |                  | ``cover``  | Default: None                                           |
@@ -340,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_autotune.py b/sbysrc/sby_autotune.py
index 9e2f28c..c7d741c 100644
--- a/sbysrc/sby_autotune.py
+++ b/sbysrc/sby_autotune.py
@@ -391,7 +391,7 @@ class SbyAutotune:
         else:
             self.task.copy_src()
 
-        self.model(None, "base")
+        self.model(None, "prep")
         self.task.taskloop.run()
 
         if self.task.status == "ERROR":
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 790d64d..366817f 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -81,6 +81,7 @@ class SbyProc:
         self.linebuffer = ""
         self.logstderr = logstderr
         self.silent = silent
+        self.wait = False
 
         self.task.update_proc_pending(self)
 
@@ -130,7 +131,7 @@ class SbyProc:
             self.error_callback(retcode)
 
     def terminate(self, timeout=False):
-        if self.task.opt_wait and not timeout:
+        if (self.task.opt_wait or self.wait) and not timeout:
             return
         if self.running:
             if not self.silent:
@@ -585,25 +586,43 @@ class SbyTask(SbyConfig):
         if not os.path.isdir(f"{self.workdir}/model"):
             os.makedirs(f"{self.workdir}/model")
 
-        def print_common_prep(check):
-            print("scc -select; simplemap; select -clear", file=f)
-            if self.opt_multiclock:
-                print("clk2fflogic", file=f)
-            else:
-                print("async2sync", file=f)
-                print("chformal -assume -early", file=f)
-            if self.opt_mode in ["bmc", "prove"]:
-                print("chformal -live -fair -cover -remove", file=f)
-            if self.opt_mode == "cover":
-                print("chformal -live -fair -remove", file=f)
-            if self.opt_mode == "live":
-                print("chformal -assert2assume", file=f)
-                print("chformal -cover -remove", file=f)
-            print("opt_clean", file=f)
-            print("setundef -anyseq", file=f)
-            print("opt -keepdc -fast", file=f)
-            print("check", file=f)
-            print(f"hierarchy {check}", file=f)
+        if model_name == "prep":
+            with open(f"""{self.workdir}/model/design_prep.ys""", "w") as f:
+                print(f"# running in {self.workdir}/model/", file=f)
+                print(f"""read_ilang design.il""", file=f)
+                print("scc -select; simplemap; select -clear", file=f)
+                print("memory_nordff", file=f)
+                if self.opt_multiclock:
+                    print("clk2fflogic", file=f)
+                else:
+                    print("async2sync", file=f)
+                    print("chformal -assume -early", 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":
+                    print("chformal -live -fair -remove", file=f)
+                if self.opt_mode == "live":
+                    print("chformal -assert2assume", file=f)
+                    print("chformal -cover -remove", file=f)
+                print("opt_clean", file=f)
+                print("check", file=f)  # can't detect undriven wires past this point
+                print("setundef -undriven -anyseq", file=f)
+                print("opt -fast", file=f)
+                print("rename -witness", file=f)
+                print("opt_clean", file=f)
+                print(f"""write_rtlil ../model/design_prep.il""", file=f)
+
+            proc = SbyProc(
+                self,
+                model_name,
+                self.model("base"),
+                "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)
+            )
+            proc.checkretcode = True
+
+            return [proc]
 
         if model_name == "base":
             with open(f"""{self.workdir}/model/design.ys""", "w") as f:
@@ -639,12 +658,11 @@ class SbyTask(SbyConfig):
         if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name):
             with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f:
                 print(f"# running in {self.workdir}/model/", file=f)
-                print(f"""read_ilang design.il""", file=f)
+                print(f"""read_ilang design_prep.il""", file=f)
+                print("hierarchy -smtcheck", file=f)
                 if "_nomem" in model_name:
-                    print("memory_map", file=f)
-                else:
-                    print("memory_nordff", file=f)
-                print_common_prep("-smtcheck")
+                    print("memory_map -formal", file=f)
+                    print("formalff -setundef -clk2ff -ff2anyinit", file=f)
                 if "_syn" in model_name:
                     print("techmap", file=f)
                     print("opt -fast", file=f)
@@ -662,7 +680,7 @@ class SbyTask(SbyConfig):
             proc = SbyProc(
                 self,
                 model_name,
-                self.model("base"),
+                self.model("prep"),
                 "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)
             )
             proc.checkretcode = True
@@ -672,12 +690,11 @@ class SbyTask(SbyConfig):
         if re.match(r"^btor(_syn)?(_nomem)?$", model_name):
             with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f:
                 print(f"# running in {self.workdir}/model/", file=f)
-                print(f"""read_ilang design.il""", file=f)
+                print(f"""read_ilang design_prep.il""", file=f)
+                print("hierarchy -simcheck", file=f)
                 if "_nomem" in model_name:
-                    print("memory_map", file=f)
-                else:
-                    print("memory_nordff", file=f)
-                print_common_prep("-simcheck")
+                    print("memory_map -formal", file=f)
+                    print("formalff -setundef -clk2ff -ff2anyinit", file=f)
                 print("flatten", file=f)
                 print("setundef -undriven -anyseq", file=f)
                 if "_syn" in model_name:
@@ -687,7 +704,7 @@ class SbyTask(SbyConfig):
                     print("abc", file=f)
                     print("opt_clean", file=f)
                 else:
-                    print("opt -fast -keepdc", file=f)
+                    print("opt -fast", file=f)
                 print("delete -output", file=f)
                 print("dffunmap", file=f)
                 print("stat", file=f)
@@ -697,7 +714,7 @@ class SbyTask(SbyConfig):
             proc = SbyProc(
                 self,
                 model_name,
-                self.model("base"),
+                self.model("prep"),
                 "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)
             )
             proc.checkretcode = True
@@ -707,9 +724,8 @@ class SbyTask(SbyConfig):
         if model_name == "aig":
             with open(f"{self.workdir}/model/design_aiger.ys", "w") as f:
                 print(f"# running in {self.workdir}/model/", file=f)
-                print("read_ilang design.il", file=f)
-                print("memory_map", file=f)
-                print_common_prep("-simcheck")
+                print("read_ilang design_prep.il", file=f)
+                print("hierarchy -simcheck", file=f)
                 print("flatten", file=f)
                 print("setundef -undriven -anyseq", file=f)
                 print("setattr -unset keep", file=f)
@@ -717,23 +733,26 @@ class SbyTask(SbyConfig):
                 print("opt -full", file=f)
                 print("techmap", file=f)
                 print("opt -fast", file=f)
+                print("memory_map -formal", file=f)
+                print("formalff -clk2ff -ff2anyinit", file=f)
+                print("simplemap", file=f)
                 print("dffunmap", file=f)
                 print("abc -g AND -fast", file=f)
                 print("opt_clean", file=f)
                 print("stat", file=f)
-                print("write_aiger -I -B -zinit -no-startoffset -map design_aiger.aim design_aiger.aig", file=f)
+                print("write_aiger -I -B -zinit -no-startoffset -map design_aiger.aim -ywmap design_aiger.ywa design_aiger.aig", file=f)
 
             proc = SbyProc(
                 self,
                 "aig",
-                self.model("base"),
+                self.model("prep"),
                 f"""cd {self.workdir}/model; {self.exe_paths["yosys"]} -ql design_aiger.log design_aiger.ys"""
             )
             proc.checkretcode = True
 
             return [proc]
 
-        assert False
+        self.error(f"Invalid model name: {model_name}")
 
     def model(self, model_name):
         if model_name not in self.models:
@@ -811,6 +830,8 @@ class SbyTask(SbyConfig):
         self.handle_int_option("skip", None)
         self.handle_str_option("tbtop", None)
 
+        self.handle_str_option("make_model", None)
+
     def setup_procs(self, setupmode):
         self.handle_non_engine_options()
         if self.opt_smtc is not None:
@@ -838,6 +859,13 @@ class SbyTask(SbyConfig):
             self.retcode = 0
             return
 
+        if self.opt_make_model is not None:
+            for name in self.opt_make_model.split(","):
+                self.model(name.strip())
+
+            for proc in self.procs_pending:
+                proc.wait = True
+
         if self.opt_mode == "bmc":
             import sby_mode_bmc
             sby_mode_bmc.run(self)
@@ -906,6 +934,8 @@ class SbyTask(SbyConfig):
 
     def print_junit_result(self, f, junit_ts_name, junit_tc_name, junit_format_strict=False):
         junit_time = strftime('%Y-%m-%dT%H:%M:%S')
+        if not self.design:
+            self.precise_prop_status = False
         if self.precise_prop_status:
             checks = self.design.hierarchy.get_property_list()
             junit_tests = len(checks)
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index e392932..d59105a 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -111,7 +111,7 @@ def run(mode, task, engine_idx, engine):
                         f"engine_{engine_idx}",
                         task.model("smt2"),
                         ("cd {}; {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
-                             "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
+                             "--dump-smtc engine_{i}/trace.smtc --dump-yw engine_{i}/trace.yw --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
                                     (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
                                     "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
                                     i=engine_idx),
@@ -123,7 +123,7 @@ def run(mode, task, engine_idx, engine):
                         f"engine_{engine_idx}",
                         task.model("smt2"),
                         ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
-                             "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
+                             "--dump-smtc engine_{i}/trace.smtc --dump-yw engine_{i}/trace.yw --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
                                     (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt,
                                     "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}",
                                     task.opt_append, i=engine_idx),
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 8c11388..9dd92c3 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -152,7 +152,7 @@ def run(mode, task, engine_idx, engine):
         task,
         procname,
         task.model(model_name),
-        f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""",
+        f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --dump-vcd {trace_prefix}.vcd --dump-yw {trace_prefix}.yw --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""",
         logfile=open(logfile_prefix + ".txt", "w"),
         logstderr=(not progress)
     )
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.")
diff --git a/tests/unsorted/mixed.v b/tests/unsorted/mixed.v
index fa3cf2c..26bf3c9 100644
--- a/tests/unsorted/mixed.v
+++ b/tests/unsorted/mixed.v
@@ -1,17 +1,16 @@
-module test (input CP, CN, CX, input A, B, output reg XP, XN, YP, YN);
+module test (input CP, CN, input A, B, output reg XP, XN);
+	reg [7:0] counter = 0;
 	always @* begin
 		assume (A || B);
 		assume (!A || !B);
 		assert (A != B);
-		cover (A);
-		cover (B);
+		cover (counter == 3 && A);
+		cover (counter == 3 && B);
 	end
+	always @(posedge CP)
+		counter <= counter + 1;
 	always @(posedge CP)
 		XP <= A;
 	always @(negedge CN)
 		XN <= B;
-	always @(posedge CX)
-		YP <= A;
-	always @(negedge CX)
-		YN <= B;
 endmodule