From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 12 Sep 2018 11:12:24 +0000 (+0200)
Subject: Add "skip" options (smtbmc only)
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bf47da495b44d592615a1e6a7b92d23ab30a48f0;p=SymbiYosys.git

Add "skip" options (smtbmc only)

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 9d2871c..5143fd8 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -159,6 +159,10 @@ options are:
 |                  |            | engine. Other engines ignore this option in ``prove``   |
 |                  |            | mode. Default: ``20``                                   |
 +------------------+------------+---------------------------------------------------------+
+| ``skip``         | ``bmc``,   | Skip the specified number of time steps. Only valid     |
+|                  | ``cover``  | with smtbmc engine. All other engines are disabled when |
+|                  |            | this option is used. Default: None                      |
++------------------+------------+---------------------------------------------------------+
 | ``append``       | ``bmc``,   | When generating a counter-example trace, add the        |
 |                  | ``prove``, | specified number of cycles at the end of the trace.     |
 |                  | ``cover``  | Default: ``0``                                          |
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 16462a4..f2792ad 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -497,6 +497,7 @@ class SbyJob:
         self.handle_int_option("timeout", None)
 
         self.handle_str_option("smtc", None)
+        self.handle_int_option("skip", None)
         self.handle_str_option("tbtop", None)
 
         if self.opt_smtc is not None:
@@ -504,6 +505,14 @@ class SbyJob:
                 if engine[0] != "smtbmc":
                     self.error("Option smtc is only valid for smtbmc engine.")
 
+        if self.opt_skip is not None:
+            if self.opt_skip == 0:
+                self.opt_skip = None
+            else:
+                for engine in self.engines:
+                    if engine[0] != "smtbmc":
+                        self.error("Option skip is only valid for smtbmc engine.")
+
         self.copy_src()
 
         if self.opt_mode == "bmc":
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index bea1123..ec83c27 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -121,9 +121,15 @@ def run(mode, job, engine_idx, engine):
     if not progress:
         smtbmc_opts.append("--noprogress")
 
+
+    if job.opt_skip is not None:
+        t_opt = "%d:%d" % (job.opt_skip, job.opt_depth)
+    else:
+        t_opt = "%d" % job.opt_depth
+
     task = SbyTask(job, taskname, job.model(model_name),
-            "cd %s; %s %s -t %d --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
-                    (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name),
+            "cd %s; %s %s -t %s --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
+                    (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name),
             logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress))
 
     if mode == "prove_basecase":