From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 25 Feb 2017 14:06:47 +0000 (+0100)
Subject: Add aigsmt option
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eb83a1b90eafb738d826fd41b7246a18f1765a35;p=SymbiYosys.git

Add aigsmt option
---

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 092a176..90f399a 100644
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -81,9 +81,9 @@ def run(mode, job, engine_idx, engine):
 
         if task_status == "FAIL":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                    ("cd %s; %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; %s -s %s --noprogress --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") %
-                            (job.workdir, job.exe_paths["smtbmc"], engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx),
                     logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
 
             task2_status = None
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index c1feebd..8161be9 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -75,9 +75,9 @@ def run(mode, job, engine_idx, engine):
 
         if task_status == "FAIL":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
-                    ("cd %s; %s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
+                    ("cd %s; %s -s %s --noprogress --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 model/design_smt2.smt2") %
-                            (job.workdir, job.exe_paths["smtbmc"], engine_idx, engine_idx, engine_idx, engine_idx),
+                            (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, engine_idx, engine_idx, engine_idx, engine_idx),
                     logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
 
             task2_status = None
diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index 9a69127..2daa299 100644
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -21,10 +21,14 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_aigsmt = "z3"
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "aigsmt" in job.options:
+        job.opt_aigsmt = job.options["aigsmt"]
+
     for engine_idx in range(len(job.engines)):
         engine = job.engines[engine_idx]
         assert len(engine) > 0
diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index 67cb7f2..26eb80d 100644
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -21,10 +21,14 @@ from sby_core import SbyTask
 
 def run(job):
     job.opt_depth = 20
+    job.opt_aigsmt = "z3"
 
     if "depth" in job.options:
         job.opt_depth = int(job.options["depth"])
 
+    if "aigsmt" in job.options:
+        job.opt_aigsmt = job.options["aigsmt"]
+
     job.status = "UNKNOWN"
 
     job.basecase_pass = False