diff options
| -rw-r--r-- | backends/smt2/example.v | 11 | ||||
| -rw-r--r-- | backends/smt2/example.ys | 3 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 110 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 285 |
4 files changed, 409 insertions, 0 deletions
diff --git a/backends/smt2/example.v b/backends/smt2/example.v new file mode 100644 index 00000000..b195266e --- /dev/null +++ b/backends/smt2/example.v @@ -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 diff --git a/backends/smt2/example.ys b/backends/smt2/example.ys new file mode 100644 index 00000000..6fccb344 --- /dev/null +++ b/backends/smt2/example.ys @@ -0,0 +1,3 @@ +read_verilog -formal example.v +hierarchy; proc; opt; memory -nordff -nomap; opt -fast +write_smt2 -bv -mem -wires example.smt2 diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py new file mode 100644 index 00000000..283d1231 --- /dev/null +++ b/backends/smt2/smtbmc.py @@ -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() + diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py new file mode 100644 index 00000000..774984f2 --- /dev/null +++ b/backends/smt2/smtio.py @@ -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) + |