mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Implemented smtbmc.py -i

Browse source
This commit is contained in:
Clifford Wolf 2015-10-14 00:18:38 +02:00
parent 29160525aa
commit 7bcd2a4bb3
1 changed files with 60 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

85
backends/smt2/smtbmc.py
View file

@ -3,23 +3,25 @@
import os, sys, getopt, re import os, sys, getopt, re
from smtio import smtio, smtopts, mkvcd from smtio import smtio, smtopts, mkvcd
steps = 20 max_steps = 20
min_steps = None
vcdfile = None vcdfile = None
tempind = False tempind = False
topmod = "main" topmod = "main"
so = smtopts() so = smtopts()
def usage(): def usage():
print(""" print("""
python3 smtbmc.py [options] <yosys_smt2_output> python3 smtbmc.py [options] <yosys_smt2_output>
-t <steps> -t <max_steps>
default: 20 default: 20
-c <vcd_filename> -c <vcd_filename>
write counter-example to this VCD file write counter-example to this VCD file
-i -i <min_steps>
instead of BMC run temporal induction instead of BMC run temporal induction
-m <module_name> -m <module_name>
@ -27,20 +29,20 @@ python3 smtbmc.py [options] <yosys_smt2_output>
""" + so.helpmsg()) """ + so.helpmsg())
sys.exit(1) sys.exit(1)
try: 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: except:
usage() usage()
for o, a in opts: for o, a in opts:
if o == "-t": if o == "-t":
steps = int(a) max_steps = int(a)
elif o == "-c": elif o == "-c":
vcdfile = a vcdfile = a
elif o == "-i": elif o == "-i":
tempind = True tempind = True
print("FIXME: temporal induction not yet implemented!") min_steps = int(a)
assert False
elif so.handle(o, a): elif so.handle(o, a):
pass pass
else: else:
@ -49,6 +51,7 @@ for o, a in opts:
if len(args) != 1: if len(args) != 1:
usage() usage()
smt = smtio(opts=so) smt = smtio(opts=so)
print("Solver: %s" % so.solver) print("Solver: %s" % so.solver)
@ -64,6 +67,7 @@ with open(args[0], "r") as f:
debug_nets.add(match.group(2)) debug_nets.add(match.group(2))
smt.write(line) smt.write(line)
def write_vcd_model(): def write_vcd_model():
print("%s Writing model to VCD file." % smt.timestamp()) print("%s Writing model to VCD file." % smt.timestamp())
@ -79,30 +83,61 @@ def write_vcd_model():
vcd.set_time(step+1) 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: if tempind:
smt.write("(assert (%s_i s0))" % (topmod)) 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: if step == max_steps:
smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step)) smt.write("(assert (not (%s_a s%d)))" % (topmod, step))
print("%s Checking sequence of length %d.." % (smt.timestamp(), step)) else:
smt.write("(push 1)") smt.write("(assert (%s_t s%d s%d))" % (topmod, step, step+1))
smt.write("(assert (%s_a s%d))" % (topmod, step))
smt.write("(assert (not (%s_a s%d)))" % (topmod, step)) if step > max_steps-min_steps:
print("%s Skipping induction in step %d.." % (smt.timestamp(), step))
continue
if smt.check_sat() == "sat": print("%s Trying induction in step %d.." % (smt.timestamp(), step))
print("%s BMC failed!" % smt.timestamp())
if vcdfile is not None: if smt.check_sat() == "sat":
write_vcd_model() if step == 0:
break 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)")
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
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()) print("%s Done." % smt.timestamp())
smt.write("(exit)") smt.write("(exit)")