From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 4 Mar 2018 13:08:55 +0000 (+0100)
Subject: Add smtbmc --stdt option
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e966f3dca490fed40fc6df3677e4ec60c382c1ba;p=SymbiYosys.git

Add smtbmc --stdt option

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index c8951e5..ca8075a 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -110,6 +110,8 @@ the following options:
 | ``--stbv``      | Use large bit vectors (instead of uninterpreted         |
 |                 | functions) to represent the circuit state.              |
 +-----------------+---------------------------------------------------------+
+| ``--stdt``      | Use SMT-LIB 2.6 datatypes to represent states.          |
++-----------------+---------------------------------------------------------+
 | ``--nopresat``  | Do not run "presat" SMT queries that make sure that     |
 |                 | assumptions are non-conflicting (and potentially        |
 |                 | warmup the SMT solver).                                 |
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 3cb37b5..cbb7e07 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -368,7 +368,7 @@ class SbyJob:
 
             return [task]
 
-        if re.match(r"^smt2(_syn)?(_nomem)?(_stbv)?$", model_name):
+        if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name):
             with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f:
                 print("# running in %s/model/" % (self.workdir), file=f)
                 print("read_ilang design.il", file=f)
@@ -383,6 +383,8 @@ class SbyJob:
                 print("stat", file=f)
                 if "_stbv" in model_name:
                     print("write_smt2 -stbv -wires design_%s.smt2" % model_name, file=f)
+                elif "_stdt" in model_name:
+                    print("write_smt2 -stdt -wires design_%s.smt2" % model_name, file=f)
                 else:
                     print("write_smt2 -wires design_%s.smt2" % model_name, file=f)
 
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 48431aa..be04515 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -26,9 +26,10 @@ def run(mode, job, engine_idx, engine):
     unroll_opt = None
     syn_opt = False
     stbv_opt = False
+    stdt_opt = False
     dumpsmt2 = False
 
-    opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "presat", "nopresat", "unroll", "nounroll", "dumpsmt2"])
+    opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat", "nopresat", "unroll", "nounroll", "dumpsmt2"])
 
     for o, a in opts:
         if o == "--nomem":
@@ -37,6 +38,8 @@ def run(mode, job, engine_idx, engine):
             syn_opt = True
         elif o == "--stbv":
             stbv_opt = True
+        elif o == "--stdt":
+            stdt_opt = True
         elif o == "--presat":
             presat_opt = True
         elif o == "--nopresat":
@@ -71,6 +74,7 @@ def run(mode, job, engine_idx, engine):
     if syn_opt: model_name += "_syn"
     if nomem_opt: model_name += "_nomem"
     if stbv_opt: model_name += "_stbv"
+    if stdt_opt: model_name += "_stdt"
 
     if mode == "prove":
         run("prove_basecase", job, engine_idx, engine)