summaryrefslogtreecommitdiff
path: root/backends/smt2
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2015-10-14 00:18:38 +0200
committerClifford Wolf <clifford@clifford.at>2015-10-14 00:18:38 +0200
commit7bcd2a4bb3592e8a472fb63e4cd1cc47cdc50de4 (patch)
tree9e41807f316a6c84ecbb55d69073d2a703636eaa /backends/smt2
parent29160525aaf99af331412d3810e3a6931aa20ac7 (diff)
Implemented smtbmc.py -i
Diffstat (limited to 'backends/smt2')
-rw-r--r--backends/smt2/smtbmc.py85
1 files changed, 60 insertions, 25 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 283d1231..80c2c3cf 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -3,23 +3,25 @@
import os, sys, getopt, re
from smtio import smtio, smtopts, mkvcd
-steps = 20
+max_steps = 20
+min_steps = None
vcdfile = None
tempind = False
topmod = "main"
so = smtopts()
+
def usage():
print("""
python3 smtbmc.py [options] <yosys_smt2_output>
- -t <steps>
+ -t <max_steps>
default: 20
-c <vcd_filename>
write counter-example to this VCD file
- -i
+ -i <min_steps>
instead of BMC run temporal induction
-m <module_name>
@@ -27,20 +29,20 @@ python3 smtbmc.py [options] <yosys_smt2_output>
""" + so.helpmsg())
sys.exit(1)
+
try:
- opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:c:im:")
+ opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:c:i:m:")
except:
usage()
for o, a in opts:
if o == "-t":
- steps = int(a)
+ max_steps = int(a)
elif o == "-c":
vcdfile = a
elif o == "-i":
tempind = True
- print("FIXME: temporal induction not yet implemented!")
- assert False
+ min_steps = int(a)
elif so.handle(o, a):
pass
else:
@@ -49,6 +51,7 @@ for o, a in opts:
if len(args) != 1:
usage()
+
smt = smtio(opts=so)
print("Solver: %s" % so.solver)
@@ -64,6 +67,7 @@ with open(args[0], "r") as f:
debug_nets.add(match.group(2))
smt.write(line)
+
def write_vcd_model():
print("%s Writing model to VCD file." % smt.timestamp())
@@ -79,30 +83,61 @@ def write_vcd_model():
vcd.set_time(step+1)
-for step in range(steps):
- smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
- smt.write("(assert (%s_u s0))" % (topmod))
- if step == 0:
- smt.write("(assert (%s_i s0))" % (topmod))
+if tempind:
+ for step in range(max_steps, -1, -1):
+ smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
+ smt.write("(assert (%s_u s%d))" % (topmod, step))
- else:
- smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
+ if step == max_steps:
+ smt.write("(assert (not (%s_a s%d)))" % (topmod, step))
+
+ else:
+ smt.write("(assert (%s_t s%d s%d))" % (topmod, step, step+1))
+ smt.write("(assert (%s_a s%d))" % (topmod, step))
+
+ if step > max_steps-min_steps:
+ print("%s Skipping induction in step %d.." % (smt.timestamp(), step))
+ continue
+
+ print("%s Trying induction in step %d.." % (smt.timestamp(), step))
+
+ if smt.check_sat() == "sat":
+ if step == 0:
+ print("%s temporal induction failed!" % smt.timestamp())
+ if vcdfile is not None:
+ write_vcd_model()
+
+ else:
+ print("%s PASSED." % smt.timestamp())
+ break
+
+else: # not tempind
+ for step in range(max_steps+1):
+ smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
+ smt.write("(assert (%s_u s%d))" % (topmod, step))
+
+ if step == 0:
+ smt.write("(assert (%s_i s0))" % (topmod))
+
+ else:
+ smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
+
+ print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
+ smt.write("(push 1)")
- print("%s Checking sequence of length %d.." % (smt.timestamp(), step))
- smt.write("(push 1)")
+ smt.write("(assert (not (%s_a s%d)))" % (topmod, step))
- smt.write("(assert (not (%s_a s%d)))" % (topmod, step))
+ if smt.check_sat() == "sat":
+ print("%s BMC failed!" % smt.timestamp())
+ if vcdfile is not None:
+ write_vcd_model()
+ break
- if smt.check_sat() == "sat":
- print("%s BMC failed!" % smt.timestamp())
- if vcdfile is not None:
- write_vcd_model()
- break
+ else: # unsat
+ smt.write("(pop 1)")
+ smt.write("(assert (%s_a s%d))" % (topmod, step))
- else: # unsat
- smt.write("(pop 1)")
- smt.write("(assert (%s_a s%d))" % (topmod, step))
print("%s Done." % smt.timestamp())
smt.write("(exit)")