From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 23 Oct 2017 00:17:39 +0000 (+0200)
Subject: Add "smtbmc --dumpsmt2"
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78efd64985a2979edc42ef0ccde98634fbb45a0b;p=SymbiYosys.git

Add "smtbmc --dumpsmt2"
---

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index cc44f28..3731dc5 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -24,8 +24,9 @@ def run(mode, job, engine_idx, engine):
     nomem_opt = False
     syn_opt = False
     stbv_opt = False
+    dumpsmt2 = False
 
-    opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "presat", "unroll"])
+    opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "presat", "unroll", "dumpsmt2"])
 
     for o, a in opts:
         if o == "--nomem":
@@ -38,6 +39,8 @@ def run(mode, job, engine_idx, engine):
             smtbmc_opts += ["--presat"]
         elif o == "--unroll":
             smtbmc_opts += ["--unroll"]
+        elif o == "--dumpsmt2":
+            dumpsmt2 = True
         else:
             assert False
 
@@ -78,6 +81,9 @@ def run(mode, job, engine_idx, engine):
         smtbmc_opts.append("-c")
         trace_prefix += "%"
 
+    if dumpsmt2:
+        smtbmc_opts += ["--dump-smt2", trace_prefix + ".smt2"]
+
     task = SbyTask(job, taskname, job.model(model_name),
             "cd %s; %s --noprogress %s -t %d --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
                     (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name),