From 6ef12a4b31d16bb2c9f9776f5348213ba2ea6a1a Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 1 Jul 2017 18:33:36 +0200
Subject: [PATCH] Add tbtop config option

---
 docs/source/reference.rst   |  3 +++
 sbysrc/sby_core.py          |  1 +
 sbysrc/sby_engine_abc.py    |  6 ++++--
 sbysrc/sby_engine_aiger.py  | 12 ++++++++----
 sbysrc/sby_engine_smtbmc.py |  3 +++
 5 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 0ddbaaa..7a48112 100644
--- 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 a1039a4..9f264be 100644
--- 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 4d9b2d3..6e5bb09 100644
--- 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 af4501b..d67a9c6 100644
--- 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 dce23e4..ba0fc12 100644
--- 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"
-- 
2.30.2