diff --git a/scripts/smt2-bmc/async.py b/scripts/smt2-bmc/async.py index d088428..c60cf15 100644 --- a/scripts/smt2-bmc/async.py +++ b/scripts/smt2-bmc/async.py @@ -1,41 +1,24 @@ #!/usr/bin/env python3 import os, sys, getopt -from time import time -from smtio import smtio +from smtio import smtio, smtopts steps = 12 words = 0 -solver = "yices" allmem = False fastmem = False initzero = False check_mem = True check_regs = True -timeinfo = True -debug_print = False -debug_file = None +so = smtopts() def usage(): print(""" python3 async.py [options] - -s - set SMT solver: yices, z3, cvc4, mathsat - default: yices - -t default: 12 - - -v - enable debug output - - -p - disable timer display during solving - - -d - write smt2 statements to debug.smt2 -""") +""" + so.helpmsg()) sys.exit(1) try: @@ -44,30 +27,19 @@ except: usage() for o, a in opts: - if o == "-s": - solver = a - elif o == "-t": + if o == "-t": steps = int(a) - elif o == "-v": - debug_print = True - elif o == "-d": - debug_file = open("debug.smt2", "w") - elif o == "-p": - timeinfo = False + elif so.handle(o, a): + pass else: usage() if len(args) > 0: usage() -start_time = time() -smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file, timeinfo=timeinfo) +smt = smtio(opts=so) -def timestamp(): - secs = int(time() - start_time) - return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) - -print("Solver: %s" % solver) +print("Solver: %s" % so.solver) smt.setup("QF_AUFBV", "PicoRV32 \"async.py\" BMC script, powered by Yosys") regs_a = list() @@ -121,7 +93,7 @@ for step in range(steps): smt.write("(assert (|main_a_n resetn| a%d))" % step) smt.write("(assert (|main_b_n resetn| b%d))" % step) - print("%s Checking sequence of length %d.." % (timestamp(), step)) + print("%s Checking sequence of length %d.." % (smt.timestamp(), step)) smt.write("(push 1)") # stop with a trap and no pending memory xfer @@ -143,7 +115,7 @@ for step in range(steps): if smt.check_sat() == "sat": - print("%s Creating model.." % timestamp()) + print("%s Creating model.." % smt.timestamp()) def make_cpu_regs(step): for i in range(1, 32): @@ -355,7 +327,7 @@ for step in range(steps): else: # unsat smt.write("(pop 1)") -print("%s Done." % timestamp()) +print("%s Done." % smt.timestamp()) smt.write("(exit)") smt.wait() diff --git a/scripts/smt2-bmc/smtio.py b/scripts/smt2-bmc/smtio.py index 2a63703..e223e85 100644 --- a/scripts/smt2-bmc/smtio.py +++ b/scripts/smt2-bmc/smtio.py @@ -3,25 +3,48 @@ import sys import subprocess from select import select +from time import time class smtio: - def __init__(self, solver="yices", debug_print=False, debug_file=None, timeinfo=True): - if solver == "yices": + 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 = "yices" + 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 solver == "z3": + if self.solver == "z3": popen_vargs = ['z3', '-smt2', '-in'] - if solver == "cvc4": + if self.solver == "cvc4": popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] - if solver == "mathsat": + if self.solver == "mathsat": popen_vargs = ['mathsat'] - self.debug_print = debug_print - self.debug_file = debug_file - self.timeinfo = timeinfo 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) @@ -30,6 +53,10 @@ class smtio: 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: @@ -190,6 +217,43 @@ class smtio: self.p.wait() +class smtopts: + def __init__(self): + self.solver = "yices" + 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 + set SMT solver: yices, z3, cvc4, mathsat + default: yices + + -v + enable debug output + + -p + disable timer display during solving + + -d + write smt2 statements to file + """ + + class mkvcd: def __init__(self, f): self.f = f diff --git a/scripts/smt2-bmc/sync.py b/scripts/smt2-bmc/sync.py index 4482e51..eca0371 100644 --- a/scripts/smt2-bmc/sync.py +++ b/scripts/smt2-bmc/sync.py @@ -1,37 +1,20 @@ #!/usr/bin/env python3 import os, sys, getopt -from time import time -from smtio import smtio +from smtio import smtio, smtopts steps = 20 words = 0 -solver = "yices" allmem = False -timeinfo = True -debug_print = False -debug_file = None +so = smtopts() def usage(): print(""" python3 sync.py [options] - -s - set SMT solver: yices, z3, cvc4, mathsat - default: yices - -t default: 20 - - -v - enable debug output - - -p - disable timer display during solving - - -d - write smt2 statements to debug.smt2 -""") +""" + so.helpmsg()) sys.exit(1) try: @@ -40,30 +23,19 @@ except: usage() for o, a in opts: - if o == "-s": - solver = a - elif o == "-t": + if o == "-t": steps = int(a) - elif o == "-v": - debug_print = True - elif o == "-d": - debug_file = open("debug.smt2", "w") - elif o == "-p": - timeinfo = False + elif so.handle(o, a): + pass else: usage() if len(args) > 0: usage() -start_time = time() -smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file, timeinfo=timeinfo) +smt = smtio(opts=so) -def timestamp(): - secs = int(time() - start_time) - return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) - -print("Solver: %s" % solver) +print("Solver: %s" % so.solver) smt.setup("QF_AUFBV", "PicoRV32 \"sync.py\" BMC script, powered by Yosys") regs_a = list() @@ -108,7 +80,7 @@ for step in range(steps): smt.write("(assert (|main_a_n resetn| a%d))" % step) smt.write("(assert (|main_b_n resetn| b%d))" % step) - print("%s Checking sequence of length %d.." % (timestamp(), step)) + print("%s Checking sequence of length %d.." % (smt.timestamp(), step)) smt.write("(push 1)") smt.write(("(assert (or (distinct (|main_a_m cpu.cpuregs| a%d) (|main_b_m cpu.cpuregs| b%d)) " + @@ -117,7 +89,7 @@ for step in range(steps): if smt.check_sat() == "sat": - print("%s Creating model.." % timestamp()) + print("%s Creating model.." % smt.timestamp()) def make_cpu_regs(step): for i in range(1, 32): @@ -289,7 +261,7 @@ for step in range(steps): smt.write("(assert (= (|main_a_m memory| a%d) (|main_b_m memory| b%d)))" % (step, step)) smt.write("(assert (= (|main_a_n trap| a%d) (|main_b_n trap| b%d)))" % (step, step)) -print("%s Done." % timestamp()) +print("%s Done." % smt.timestamp()) smt.write("(exit)") smt.wait()