Add support for "aigsmt none" option

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index dc8c08efa3391cc06f83d71aa591d9b94474855c..0ddbaaa7d22ca171179c81b6013d6aa044eb7682 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -20,6 +20,8 @@ Mode      Description
 ``prove`` Unbounded model check to verify safety properties (``assert(...)`` statements)
 ``live``  Unbounded model check to verify liveness properties (``assert(s_eventually ...)`` statements)
 ``cover`` Generate set of shortest traces required to reach all cover() statements
+``equiv`` Formal equivalence checking (usually to verify pre- and post-synthesis equivalence)
+``synth`` Reactive Synthesis (synthesis of circuit from safety properties)
 ========= ===========
 
 All other options have default values and thus are optional. The available
@@ -40,7 +42,8 @@ options are:
 |             |            | consistency. Values: ``on``, ``off``. Default: ``off``  |
 +-------------+------------+---------------------------------------------------------+
 | ``aigsmt``  |   All      | Which SMT2 solver to use for converting AIGER witnesses |
-|             |            | to counter example traces. Default: ``yices``           |
+|             |            | to counter example traces. Use ``none`` to disable      |
+|             |            | conversion of AIGER witnesses. Default: ``yices``       |
 +-------------+------------+---------------------------------------------------------+
 | ``smtc``    | ``bmc``,   | Pass this ``.smtc`` file to the smtbmc engine. All      |
 |             | ``prove``, | other engines are disabled when this option is used.    |

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index c1d130c1e652e4586209f84d312a6f26614e4c98..4d9b2d3d3defcb5978f47c112be31ec2152acc54 100644 (file)
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -79,7 +79,7 @@ def run(mode, job, engine_idx, engine):
 
         job.terminate()
 
-        if task_status == "FAIL":
+        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 " +
                      "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") %

diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index 97b637e279da6f496807332fd73216a665fdbdf1..af4501b63634106bf741fefb49bcf1bc2e52862a 100644 (file)
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -87,7 +87,7 @@ def run(mode, job, engine_idx, engine):
 
         job.terminate()
 
-        if task_status == "FAIL":
+        if task_status == "FAIL" and job.opt_aigsmt != "none":
             if produced_cex:
                 if mode == "live":
                     task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),