From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 7 Jul 2017 00:47:30 +0000 (+0200)
Subject: Add "yosys-smtbmc --presat"
X-Git-Tag: yosys-0.8~396
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8f7404f82c324bd4c7e88fa59fb3c5e1061ae402;p=yosys.git

Add "yosys-smtbmc --presat"
---

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index adf747034..6060d049d 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -44,6 +44,7 @@ assume_skipped = None
 final_only = False
 topmod = None
 noinfo = False
+presat = False
 so = SmtOpts()
 
 
@@ -92,6 +93,13 @@ yosys-smtbmc [options] <yosys_smt2_output>
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
 
+    --presat
+        check if the design with assumptions but without assertions
+        is SAT before checking if assertions are UNSAT. This will
+        detect if there are contradicting assumtions. In some cases
+        this will also help to "warmup" the solver, potentially
+        yielding a speedup.
+
     --final-only
         only check final constraints, assume base case
 
@@ -131,7 +139,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader",
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
              "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append="])
 except:
     usage()
@@ -177,6 +185,8 @@ for o, a in opts:
         outconstr = a
     elif o == "--dump-all":
         dumpall = True
+    elif o == "--presat":
+        presat = True
     elif o == "--noinfo":
         noinfo = True
     elif o == "--append":
@@ -1103,6 +1113,17 @@ else:  # not tempind, covermode
                 last_check_step = step+i
 
         if not gentrace:
+            if presat:
+                if last_check_step == step:
+                    print_msg("Checking assumptions in step %d.." % (step))
+                else:
+                    print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
+
+                if smt.check_sat() == "unsat":
+                    print("%s Warmup failed!" % smt.timestamp())
+                    retstatus = False
+                    break
+
             if not final_only:
                 if last_check_step == step:
                     print_msg("Checking asserts in step %d.." % (step))
@@ -1124,8 +1145,7 @@ else:  # not tempind, covermode
                             smt.write("(assert (|%s_h| s%d))" % (topmod, i))
                             smt.write("(assert (|%s_t| s%d s%d))" % (topmod, i-1, i))
                             smt.write("(assert %s)" % get_constr_expr(constr_assumes, i))
-                        print_msg("Re-solving with appended steps..")
-                        assert smt.check_sat() == "sat"
+                            assert smt.check_sat() == "sat"
                     print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)