mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 14:04:07 +00:00
Code Activity

Add make_model option to generate models not required by the task

Browse source 
Useful to do custom things (like counter example minimization) but still
use sby's flow to prepare models.
This commit is contained in:
Jannis Harder 2022-08-02 17:08:53 +02:00
parent 22585b33dc
commit 231f0b80aa
2 changed files with 18 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
docs/source/reference.rst
View file

@ -153,6 +153,12 @@ options are:
| ``tbtop`` | All | The top module for generated Verilog test benches, as | | ``tbtop`` | All | The top module for generated Verilog test benches, as |
| | | hierarchical path relative to the design top module. | | | | 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 | | ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All |
| | ``prove``, | other engines are disabled when this option is used. | | | ``prove``, | other engines are disabled when this option is used. |
| | ``cover`` | Default: None | | | ``cover`` | Default: None |

14
sbysrc/sby_core.py
View file

@ -81,6 +81,7 @@ class SbyProc:
self.linebuffer = "" self.linebuffer = ""
self.logstderr = logstderr self.logstderr = logstderr
self.silent = silent self.silent = silent
self.wait = False
self.task.update_proc_pending(self) self.task.update_proc_pending(self)
@ -130,7 +131,7 @@ class SbyProc:
self.error_callback(retcode) self.error_callback(retcode)
def terminate(self, timeout=False): 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 return
if self.running: if self.running:
if not self.silent: if not self.silent:
@ -749,7 +750,7 @@ class SbyTask(SbyConfig):
return [proc] return [proc]
assert False self.error(f"Invalid model name: {model_name}")
def model(self, model_name): def model(self, model_name):
if model_name not in self.models: if model_name not in self.models:
@ -827,6 +828,8 @@ class SbyTask(SbyConfig):
self.handle_int_option("skip", None) self.handle_int_option("skip", None)
self.handle_str_option("tbtop", None) self.handle_str_option("tbtop", None)
self.handle_str_option("make_model", None)
def setup_procs(self, setupmode): def setup_procs(self, setupmode):
self.handle_non_engine_options() self.handle_non_engine_options()
if self.opt_smtc is not None: if self.opt_smtc is not None:
@ -854,6 +857,13 @@ class SbyTask(SbyConfig):
self.retcode = 0 self.retcode = 0
return 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": if self.opt_mode == "bmc":
import sby_mode_bmc import sby_mode_bmc
sby_mode_bmc.run(self) sby_mode_bmc.run(self)