Add smtbmc --progress option

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

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 1135c6d55024e16cbb2417b89223fb56bf9f082b..92292c32eb17d05f4355d1509478f1bbb53b09fa 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -222,6 +222,8 @@ the following options:
 | ``--dumpsmt2``  | Write the SMT2 trace to an additional output file.      |
 |                 | (Useful for benchmarking and troubleshooting.)          |
 +-----------------+---------------------------------------------------------+
+| ``--progress``  | Enable Yosys-SMTBMC timer display.                      |
++-----------------+---------------------------------------------------------+
 
 Any SMT2 solver that is compatible with ``yosys-smtbmc`` can be passed as
 argument to the ``smtbmc`` engine. The solver options are passed to the solver

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 0f460c1e46235ba2a894d2c0e2203cc7e8c3a3f6..8a45f451ec83978c6d3952dfd2c470c6f5ae9711 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -23,7 +23,7 @@ from select import select
 from time import time
 
 class SbyTask:
-    def __init__(self, job, info, deps, cmdline, logfile=None):
+    def __init__(self, job, info, deps, cmdline, logfile=None, logstderr=True):
         self.running = False
         self.finished = False
         self.terminated = False
@@ -36,6 +36,7 @@ class SbyTask:
         self.noprintregex = None
         self.notify = []
         self.linebuffer = ""
+        self.logstderr = logstderr
 
         for dep in self.deps:
             dep.register_dep(self)
@@ -88,7 +89,8 @@ class SbyTask:
                     return
 
             self.job.log("%s: starting process \"%s\"" % (self.info, self.cmdline))
-            self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+            self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE,
+                    stderr=(subprocess.STDOUT if self.logstderr else None))
             fl = fcntl.fcntl(self.p.stdout, fcntl.F_GETFL)
             fcntl.fcntl(self.p.stdout, fcntl.F_SETFL, fl | os.O_NONBLOCK)
             self.job.tasks_running.append(self)

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index be045156db53b60e69c690825a06abff683052cd..3d46051e41c84ad929afc3d41cd827695c02ab87 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -28,8 +28,10 @@ def run(mode, job, engine_idx, engine):
     stbv_opt = False
     stdt_opt = False
     dumpsmt2 = False
+    progress = False
 
-    opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat", "nopresat", "unroll", "nounroll", "dumpsmt2"])
+    opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
+            "nopresat", "unroll", "nounroll", "dumpsmt2", "progress"])
 
     for o, a in opts:
         if o == "--nomem":
@@ -50,6 +52,8 @@ def run(mode, job, engine_idx, engine):
             unroll_opt = False
         elif o == "--dumpsmt2":
             dumpsmt2 = True
+        elif o == "--progress":
+            progress = True
         else:
             assert False
 
@@ -102,10 +106,13 @@ def run(mode, job, engine_idx, engine):
     if dumpsmt2:
         smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"]
 
+    if not progress:
+        smtbmc_opts.append("--noprogress")
+
     task = SbyTask(job, taskname, job.model(model_name),
-            "cd %s; %s --noprogress %s -t %d --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
+            "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),
-            logfile=open(logfile_prefix + ".txt", "w"))
+            logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress))
 
     if mode == "prove_basecase":
         job.basecase_tasks.append(task)