From 4b62d4cbb93500a634deabdb4bd0fab1b90b10c0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 27 Aug 2015 12:46:02 +0200 Subject: [PATCH] Added (set-info ..) generation to smtio.py --- scripts/smt2-bmc/async.py | 22 +++++++--------------- scripts/smt2-bmc/smtio.py | 22 ++++++++++++++++++++++ scripts/smt2-bmc/sync.py | 8 +++----- 3 files changed, 32 insertions(+), 20 deletions(-) diff --git a/scripts/smt2-bmc/async.py b/scripts/smt2-bmc/async.py index 6113714..80ffb72 100644 --- a/scripts/smt2-bmc/async.py +++ b/scripts/smt2-bmc/async.py @@ -62,7 +62,7 @@ def timestamp(): return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) print("Solver: %s" % solver) -smt.write("(set-logic QF_AUFBV)") +smt.setup("QF_AUFBV", "PicoRV32 \"async.py\" BMC script, powered by Yosys") regs_a = list() regs_b = list() @@ -135,9 +135,7 @@ for step in range(steps): else: assert False - smt.write("(check-sat)") - - if smt.read() == "sat": + if smt.check_sat() == "sat": print("%s Creating model.." % timestamp()) @@ -149,8 +147,6 @@ for step in range(steps): make_cpu_regs(0) make_cpu_regs(step) - smt.write("(check-sat)") - def print_status(mod, step): resetn = smt.get_net_bool("main_" + mod, "resetn", "%s%d" % (mod, step)) memvld = smt.get_net_bool("main_" + mod, "mem_valid", "%s%d" % (mod, step)) @@ -176,7 +172,7 @@ for step in range(steps): rb = smt.bv2hex(smt.get("b%d_r%d" % (step, i))) print("%3s[%d]: A=%s B=%s%s" % ("x%d" % i, step, ra, rb, " !" if ra != rb else "")) - assert smt.read() == "sat" + assert smt.check_sat() == "sat" if initzero: for rn, rs in regs_a: @@ -188,8 +184,7 @@ for step in range(steps): smt.write("(assert (not (|main_a_n %s| a0)))" % rn) else: smt.write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs)) - smt.write("(check-sat)") - if smt.read() != "sat": + if smt.check_sat() != "sat": force_to_zero = False smt.write("(pop 1)") if force_to_zero: @@ -197,8 +192,7 @@ for step in range(steps): smt.write("(assert (not (|main_a_n %s| a0)))" % rn) else: smt.write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs)) - smt.write("(check-sat)") - assert smt.read() == "sat" + assert smt.check_sat() == "sat" for rn, rs in regs_b: force_to_zero = True if smt.get_net_bin("main_b", rn, "b0").count("1") != 0: @@ -208,8 +202,7 @@ for step in range(steps): smt.write("(assert (not (|main_b_n %s| b0)))" % rn) else: smt.write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs)) - smt.write("(check-sat)") - if smt.read() != "sat": + if smt.check_sat() != "sat": force_to_zero = False smt.write("(pop 1)") if force_to_zero: @@ -217,8 +210,7 @@ for step in range(steps): smt.write("(assert (not (|main_b_n %s| b0)))" % rn) else: smt.write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs)) - smt.write("(check-sat)") - assert smt.read() == "sat" + assert smt.check_sat() == "sat" print() print_cpu_regs(0) diff --git a/scripts/smt2-bmc/smtio.py b/scripts/smt2-bmc/smtio.py index bdd8100..dcdc3d2 100644 --- a/scripts/smt2-bmc/smtio.py +++ b/scripts/smt2-bmc/smtio.py @@ -21,6 +21,13 @@ class smtio: self.debug_file = debug_file self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + 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 write(self, stmt): stmt = stmt.strip() if self.debug_print: @@ -55,6 +62,21 @@ class smtio: 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() + 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] == '(': diff --git a/scripts/smt2-bmc/sync.py b/scripts/smt2-bmc/sync.py index d46af3a..3dbdf93 100644 --- a/scripts/smt2-bmc/sync.py +++ b/scripts/smt2-bmc/sync.py @@ -58,7 +58,7 @@ def timestamp(): return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) print("Solver: %s" % solver) -smt.write("(set-logic QF_AUFBV)") +smt.setup("QF_AUFBV", "PicoRV32 \"sync.py\" BMC script, powered by Yosys") regs_a = list() regs_b = list() @@ -108,9 +108,8 @@ for step in range(steps): smt.write(("(assert (or (distinct (|main_a_m cpu.cpuregs| a%d) (|main_b_m cpu.cpuregs| b%d)) " + "(distinct (|main_a_m memory| a%d) (|main_b_m memory| b%d))" + "(distinct (|main_a_n trap| a%d) (|main_b_n trap| b%d))))") % (step, step, step, step, step, step)) - smt.write("(check-sat)") - if smt.read() == "sat": + if smt.check_sat() == "sat": print("%s Creating model.." % timestamp()) @@ -122,8 +121,7 @@ for step in range(steps): make_cpu_regs(0) make_cpu_regs(step) - smt.write("(check-sat)") - assert smt.read() == "sat" + assert smt.sheck_sat() == "sat" def print_status(mod, step): resetn = smt.get_net_bool("main_" + mod, "resetn", "%s%d" % (mod, step))