From ff054ab88b99b21467db5a2d1352e95bc49e269b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 28 May 2017 12:32:03 +0200 Subject: [PATCH] Add support for "aigsmt none" option --- docs/source/reference.rst | 5 ++++- sbysrc/sby_engine_abc.py | 2 +- sbysrc/sby_engine_aiger.py | 2 +- 3 files changed, 6 insertions(+), 3 deletions(-) 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"), -- 2.30.2