1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
#!/usr/bin/env python3
import os, sys, getopt, re
from smtio import smtio, smtopts, mkvcd
steps = 20
vcdfile = None
tempind = False
topmod = "main"
so = smtopts()
def usage():
print("""
python3 smtbmc.py [options] <yosys_smt2_output>
-t <steps>
default: 20
-c <vcd_filename>
write counter-example to this VCD file
-i
instead of BMC run temporal induction
-m <module_name>
name of the top module, default: main
""" + so.helpmsg())
sys.exit(1)
try:
opts, args = getopt.getopt(sys.argv[1:], so.optstr + "t:c:im:")
except:
usage()
for o, a in opts:
if o == "-t":
steps = int(a)
elif o == "-c":
vcdfile = a
elif o == "-i":
tempind = True
print("FIXME: temporal induction not yet implemented!")
assert False
elif so.handle(o, a):
pass
else:
usage()
if len(args) != 1:
usage()
smt = smtio(opts=so)
print("Solver: %s" % so.solver)
smt.setup("QF_AUFBV")
debug_nets = set()
debug_nets_re = re.compile(r"^; yosys-smt2-(input|output|register|wire) (\S+) (\d+)")
with open(args[0], "r") as f:
for line in f:
match = debug_nets_re.match(line)
if match:
debug_nets.add(match.group(2))
smt.write(line)
def write_vcd_model():
print("%s Writing model to VCD file." % smt.timestamp())
vcd = mkvcd(open(vcdfile, "w"))
for netname in sorted(debug_nets):
width = len(smt.get_net_bin("main", netname, "s0"))
vcd.add_net(netname, width)
for i in range(step+1):
vcd.set_time(i)
for netname in debug_nets:
vcd.set_net(netname, smt.get_net_bin("main", netname, "s%d" % i))
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))
else:
smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step))
print("%s Checking sequence of length %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))
print("%s Done." % smt.timestamp())
smt.write("(exit)")
smt.wait()
|
