From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 28 May 2017 10:32:03 +0000 (+0200)
Subject: Add support for "aigsmt none" option
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff054ab88b99b21467db5a2d1352e95bc49e269b;p=SymbiYosys.git

Add support for "aigsmt none" option
---

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index dc8c08e..0ddbaaa 100644
--- 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 c1d130c..4d9b2d3 100644
--- 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 97b637e..af4501b 100644
--- 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"),