From 231f0b80aa15bea98987ebc47527cac8f9eb2067 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Tue, 2 Aug 2022 17:08:53 +0200
Subject: [PATCH] Add make_model option to generate models not required by the
 task

Useful to do custom things (like counter example minimization) but still
use sby's flow to prepare models.
---
 docs/source/reference.rst |  6 ++++++
 sbysrc/sby_core.py        | 14 ++++++++++++--
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 8d00314..447673a 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                                           |
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index d855abf..2a1a994 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:
@@ -749,7 +750,7 @@ class SbyTask(SbyConfig):
 
             return [proc]
 
-        assert False
+        self.error(f"Invalid model name: {model_name}")
 
     def model(self, model_name):
         if model_name not in self.models:
@@ -827,6 +828,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:
@@ -854,6 +857,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)