mirror of https://github.com/YosysHQ/yosys.git
Added smtbmc.py
This commit is contained in:
Clifford Wolf
parent
3a22b31bda
commit
29160525aa
|
|
@ -0,0 +1,11 @@
|
|||
module main(input clk);
|
||||
reg [3:0] counter = 0;
|
||||
always @(posedge clk) begin
|
||||
if (counter == 10)
|
||||
counter <= 0;
|
||||
else
|
||||
counter <= counter + 1;
|
||||
end
|
||||
assert property (counter != 15);
|
||||
// assert property (counter <= 10);
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
read_verilog -formal example.v
|
||||
hierarchy; proc; opt; memory -nordff -nomap; opt -fast
|
||||
write_smt2 -bv -mem -wires example.smt2
|
||||
|
|
@ -0,0 +1,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()
|
||||
|
||||
|
|
@ -0,0 +1,285 @@
|
|||
#!/usr/bin/env python3
|
||||
|
||||
import sys
|
||||
import subprocess
|
||||
from select import select
|
||||
from time import time
|
||||
|
||||
class smtio:
|
||||
def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
|
||||
if opts is not None:
|
||||
self.solver = opts.solver
|
||||
self.debug_print = opts.debug_print
|
||||
self.debug_file = opts.debug_file
|
||||
self.timeinfo = opts.timeinfo
|
||||
|
||||
else:
|
||||
self.solver = "z3"
|
||||
self.debug_print = False
|
||||
self.debug_file = None
|
||||
self.timeinfo = True
|
||||
|
||||
if solver is not None:
|
||||
self.solver = solver
|
||||
|
||||
if debug_print is not None:
|
||||
self.debug_print = debug_print
|
||||
|
||||
if debug_file is not None:
|
||||
self.debug_file = debug_file
|
||||
|
||||
if timeinfo is not None:
|
||||
self.timeinfo = timeinfo
|
||||
|
||||
if self.solver == "yices":
|
||||
popen_vargs = ['yices-smt2', '--incremental']
|
||||
|
||||
if self.solver == "z3":
|
||||
popen_vargs = ['z3', '-smt2', '-in']
|
||||
|
||||
if self.solver == "cvc4":
|
||||
popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
|
||||
|
||||
if self.solver == "mathsat":
|
||||
popen_vargs = ['mathsat']
|
||||
|
||||
self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
|
||||
self.start_time = time()
|
||||
|
||||
def setup(self, logic="ALL", info=None):
|
||||
self.write("(set-logic %s)" % logic)
|
||||
if info is not None:
|
||||
self.write("(set-info :source |%s|)" % info)
|
||||
self.write("(set-info :smt-lib-version 2.5)")
|
||||
self.write("(set-info :category \"industrial\")")
|
||||
|
||||
def timestamp(self):
|
||||
secs = int(time() - self.start_time)
|
||||
return "+ %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
|
||||
|
||||
def write(self, stmt):
|
||||
stmt = stmt.strip()
|
||||
if self.debug_print:
|
||||
print("> %s" % stmt)
|
||||
if self.debug_file:
|
||||
print(stmt, file=self.debug_file)
|
||||
self.debug_file.flush()
|
||||
self.p.stdin.write(bytes(stmt + "\n", "ascii"))
|
||||
self.p.stdin.flush()
|
||||
|
||||
def read(self):
|
||||
stmt = []
|
||||
count_brackets = 0
|
||||
|
||||
while True:
|
||||
line = self.p.stdout.readline().decode("ascii").strip()
|
||||
count_brackets += line.count("(")
|
||||
count_brackets -= line.count(")")
|
||||
stmt.append(line)
|
||||
if self.debug_print:
|
||||
print("< %s" % line)
|
||||
if count_brackets == 0:
|
||||
break
|
||||
if not self.p.poll():
|
||||
print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
|
||||
sys.exit(1)
|
||||
|
||||
stmt = "".join(stmt)
|
||||
if stmt.startswith("(error"):
|
||||
print("SMT Solver Error: %s" % stmt, file=sys.stderr)
|
||||
sys.exit(1)
|
||||
|
||||
return stmt
|
||||
|
||||
def check_sat(self):
|
||||
if self.debug_print:
|
||||
print("> (check-sat)")
|
||||
if self.debug_file:
|
||||
print("; running check-sat..", file=self.debug_file)
|
||||
self.debug_file.flush()
|
||||
|
||||
self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
|
||||
self.p.stdin.flush()
|
||||
|
||||
if self.timeinfo:
|
||||
i = 0
|
||||
s = "/-\|"
|
||||
|
||||
count = 0
|
||||
num_bs = 0
|
||||
while select([self.p.stdout], [], [], 0.1) == ([], [], []):
|
||||
count += 1
|
||||
|
||||
if count < 25:
|
||||
continue
|
||||
|
||||
if count % 10 == 0 or count == 25:
|
||||
secs = count // 10
|
||||
|
||||
if secs < 60:
|
||||
m = "(%d seconds)" % secs
|
||||
elif secs < 60*60:
|
||||
m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
|
||||
else:
|
||||
m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
|
||||
|
||||
print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
|
||||
num_bs = len(m) + 3
|
||||
|
||||
else:
|
||||
print("\b" + s[i], end="", file=sys.stderr)
|
||||
|
||||
sys.stderr.flush()
|
||||
i = (i + 1) % len(s)
|
||||
|
||||
if num_bs != 0:
|
||||
print("\b \b" * num_bs, end="", file=sys.stderr)
|
||||
sys.stderr.flush()
|
||||
|
||||
result = self.read()
|
||||
if self.debug_file:
|
||||
print("(set-info :status %s)" % result, file=self.debug_file)
|
||||
print("(check-sat)", file=self.debug_file)
|
||||
self.debug_file.flush()
|
||||
return result
|
||||
|
||||
def parse(self, stmt):
|
||||
def worker(stmt):
|
||||
if stmt[0] == '(':
|
||||
expr = []
|
||||
cursor = 1
|
||||
while stmt[cursor] != ')':
|
||||
el, le = worker(stmt[cursor:])
|
||||
expr.append(el)
|
||||
cursor += le
|
||||
return expr, cursor+1
|
||||
|
||||
if stmt[0] == '|':
|
||||
expr = "|"
|
||||
cursor = 1
|
||||
while stmt[cursor] != '|':
|
||||
expr += stmt[cursor]
|
||||
cursor += 1
|
||||
expr += "|"
|
||||
return expr, cursor+1
|
||||
|
||||
if stmt[0] in [" ", "\t", "\r", "\n"]:
|
||||
el, le = worker(stmt[1:])
|
||||
return el, le+1
|
||||
|
||||
expr = ""
|
||||
cursor = 0
|
||||
while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
|
||||
expr += stmt[cursor]
|
||||
cursor += 1
|
||||
return expr, cursor
|
||||
return worker(stmt)[0]
|
||||
|
||||
def bv2hex(self, v):
|
||||
if v == "true": return "1"
|
||||
if v == "false": return "0"
|
||||
h = ""
|
||||
while len(v) > 2:
|
||||
d = 0
|
||||
if len(v) > 0 and v[-1] == "1": d += 1
|
||||
if len(v) > 1 and v[-2] == "1": d += 2
|
||||
if len(v) > 2 and v[-3] == "1": d += 4
|
||||
if len(v) > 3 and v[-4] == "1": d += 8
|
||||
h = hex(d)[2:] + h
|
||||
if len(v) < 4: break
|
||||
v = v[:-4]
|
||||
return h
|
||||
|
||||
def bv2bin(self, v):
|
||||
if v == "true": return "1"
|
||||
if v == "false": return "0"
|
||||
return v[2:]
|
||||
|
||||
def get(self, expr):
|
||||
self.write("(get-value (%s))" % (expr))
|
||||
return self.parse(self.read())[0][1]
|
||||
|
||||
def get_net(self, mod_name, net_name, state_name):
|
||||
return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
|
||||
|
||||
def get_net_bool(self, mod_name, net_name, state_name):
|
||||
v = self.get_net(mod_name, net_name, state_name)
|
||||
assert v in ["true", "false"]
|
||||
return 1 if v == "true" else 0
|
||||
|
||||
def get_net_hex(self, mod_name, net_name, state_name):
|
||||
return self.bv2hex(self.get_net(mod_name, net_name, state_name))
|
||||
|
||||
def get_net_bin(self, mod_name, net_name, state_name):
|
||||
return self.bv2bin(self.get_net(mod_name, net_name, state_name))
|
||||
|
||||
def wait(self):
|
||||
self.p.wait()
|
||||
|
||||
|
||||
class smtopts:
|
||||
def __init__(self):
|
||||
self.optstr = "s:d:vp"
|
||||
self.solver = "z3"
|
||||
self.debug_print = False
|
||||
self.debug_file = None
|
||||
self.timeinfo = True
|
||||
|
||||
def handle(self, o, a):
|
||||
if o == "-s":
|
||||
self.solver = a
|
||||
elif o == "-v":
|
||||
self.debug_print = True
|
||||
elif o == "-p":
|
||||
self.timeinfo = True
|
||||
elif o == "-d":
|
||||
self.debug_file = open(a, "w")
|
||||
else:
|
||||
return False
|
||||
return True
|
||||
|
||||
def helpmsg(self):
|
||||
return """
|
||||
-s <solver>
|
||||
set SMT solver: z3, cvc4, yices, mathsat
|
||||
default: z3
|
||||
|
||||
-v
|
||||
enable debug output
|
||||
|
||||
-p
|
||||
disable timer display during solving
|
||||
|
||||
-d <filename>
|
||||
write smt2 statements to file
|
||||
"""
|
||||
|
||||
|
||||
class mkvcd:
|
||||
def __init__(self, f):
|
||||
self.f = f
|
||||
self.t = -1
|
||||
self.nets = dict()
|
||||
|
||||
def add_net(self, name, width):
|
||||
assert self.t == -1
|
||||
key = "n%d" % len(self.nets)
|
||||
self.nets[name] = (key, width)
|
||||
|
||||
def set_net(self, name, bits):
|
||||
assert name in self.nets
|
||||
assert self.t >= 0
|
||||
print("b%s %s" % (bits, self.nets[name][0]), file=self.f)
|
||||
|
||||
def set_time(self, t):
|
||||
assert t >= self.t
|
||||
if t != self.t:
|
||||
if self.t == -1:
|
||||
for name in sorted(self.nets):
|
||||
key, width = self.nets[name]
|
||||
print("$var wire %d %s %s $end" % (width, key, name), file=self.f)
|
||||
print("$enddefinitions $end", file=self.f)
|
||||
self.t = t
|
||||
assert self.t >= 0
|
||||
print("#%d" % self.t, file=self.f)
|
||||
|
||||
Loading…
Reference in New Issue