Add support for "abc sim3" engine

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 3c713f8c9d369ded7e045a80d39b2acc19329900..5c5313933a58c85eb93563f73d07a3d3e77817ef 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -33,6 +33,7 @@ class SbyTask:
         self.deps = deps
         self.cmdline = cmdline
         self.logfile = logfile
+        self.noprintregex = None
         self.notify = []
 
         for dep in self.deps:
@@ -92,8 +93,11 @@ class SbyTask:
         while True:
             outs = self.p.stdout.readline().decode("utf-8")
             if len(outs) == 0: break
-            self.job.log("%s: %s" % (self.info, outs.strip()))
-            self.handle_output(outs.strip())
+            outs = outs.strip()
+            if len(outs) == 0: continue
+            if self.noprintregex is None or not self.noprintregex.match(outs):
+                self.job.log("%s: %s" % (self.info, outs))
+            self.handle_output(outs)
 
         if self.p.poll() is not None:
             self.job.log("%s: finished (returncode=%d)" % (self.info, self.p.returncode))

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 1b122ead10ca8edb89d3820165781fd54445ee97..6490784b4de4b8ebd87e0d969d001bb46f2d3644 100644 (file)
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -20,12 +20,24 @@ import re, os, getopt
 from sby_core import SbyTask
 
 def run(mode, job, engine_idx, engine):
-    if mode == "bmc":
-        assert engine == ["abc", "bmc3"]
+    abc_opts, abc_command = getopt.getopt(engine[1:], "", [])
+
+    for o, a in abc_opts:
+        assert False
+
+    if abc_command[0] == "bmc3":
+        assert mode == "bmc"
+        assert len(abc_command) == 1
         abc_command = "bmc3 -F %d -v" % job.opt_depth
 
-    elif mode == "prove":
-        assert engine == ["abc", "pdr"]
+    elif abc_command[0] == "sim3":
+        assert mode == "bmc"
+        assert len(abc_command) == 1
+        abc_command = "sim3 -F %d -v" % job.opt_depth
+
+    elif abc_command[0] == "pdr":
+        assert mode == "prove"
+        assert len(abc_command) == 1
         abc_command = "pdr"
 
     else:
@@ -36,6 +48,7 @@ def run(mode, job, engine_idx, engine):
              "write_cex -a engine_%d/trace.aiw'") % (job.workdir, abc_command, engine_idx),
             logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w"))
 
+    task.noprintregex = re.compile(r"^\.+$")
     task_status = None
 
     def output_callback(line):