Add tbtop config option

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 0ddbaaa7d22ca171179c81b6013d6aa044eb7682..7a4811225740c43cf715806de460567b80174292 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -45,6 +45,9 @@ options are:
 |             |            | to counter example traces. Use ``none`` to disable      |
 |             |            | conversion of AIGER witnesses. Default: ``yices``       |
 +-------------+------------+---------------------------------------------------------+
+| ``tbtop``   |   All      | The top module for generated Verilog test benches, as   |
+|             |            | hierarchical path relative to the design top module.    |
++-------------+------------+---------------------------------------------------------+
 | ``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 a1039a4e9f00f029a81a4646e6bb9b8d8d4e418a..9f264be1dc13e8d45f6eda7a4d479073f4e2e050 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -463,6 +463,7 @@ class SbyJob:
         self.handle_int_option("timeout", None)
 
         self.handle_str_option("smtc", None)
+        self.handle_str_option("tbtop", None)
 
         if self.opt_smtc is not None:
             for engine in self.engines:

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 4d9b2d3d3defcb5978f47c112be31ec2152acc54..6e5bb09178126826ad8377753984dece5336093a 100644 (file)
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -81,9 +81,11 @@ def run(mode, job, engine_idx, engine):
 
         if task_status == "FAIL" and job.opt_aigsmt != "none":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                    ("cd %s; %s -s %s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; %s -s %s%s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
                      "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") %
-                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt,
+                            "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop,
+                            job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx),
                     logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
 
             task2_status = None

diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index af4501b63634106bf741fefb49bcf1bc2e52862a..d67a9c674fe471ee92c1dc6396a6fae45c4d846c 100644 (file)
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -91,15 +91,19 @@ def run(mode, job, engine_idx, engine):
             if produced_cex:
                 if mode == "live":
                     task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                            ("cd %s; %s -g -s %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                            ("cd %s; %s -g -s %s%s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
                              "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") %
-                                    (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx),
+                                    (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt,
+                                    "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop,
+                                    engine_idx, engine_idx, engine_idx, engine_idx),
                             logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
                 else:
                     task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                            ("cd %s; %s -s %s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                            ("cd %s; %s -s %s%s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
                              "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") %
-                                    (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx),
+                                    (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt,
+                                    "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop,
+                                    job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx),
                             logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
 
                 task2_status = None

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index dce23e41a50177560a8d3cde01740b90f2975657..ba0fc121d46f16a6a8046afc72a8b000d655ba69 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -43,6 +43,9 @@ def run(mode, job, engine_idx, engine):
     if job.opt_smtc is not None:
         smtbmc_opts += ["--smtc", "src/%s" % job.opt_smtc]
 
+    if job.opt_tbtop is not None:
+         smtbmc_opts += ["--vlogtb-top", job.opt_tbtop]
+
     model_name = "smt2"
     if syn_opt: model_name += "_syn"
     if nomem_opt: model_name += "_nomem"