Refactoring of scripts/smt2-bmc/

2 files changed, 220 insertions, 211 deletions

diff --git a/scripts/smt2-bmc/mem_equiv.py b/scripts/smt2-bmc/mem_equiv.py
index d40cf23..10f50c7 100644
--- a/scripts/smt2-bmc/mem_equiv.py
+++ b/scripts/smt2-bmc/mem_equiv.py
@@ -2,7 +2,7 @@
 
 import os, sys, getopt
 from time import time
-import subprocess
+from smtio import smtio
 
 steps = 15
 words = 0
@@ -10,139 +10,19 @@ solver = "yices"
 allmem = False
 fastmem = False
 initzero = False
+check_mem = True
+check_regs = True
 debug_print = False
 debug_file = open("debug.smt2", "w")
 
-
-# Yices Bindings
-#####################################
-
-if solver == "yices":
-    yices = subprocess.Popen(['yices-smt2', '--incremental'], stdin=subprocess.PIPE,
-            stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
-
-elif solver == "z3":
-    yices = subprocess.Popen(['z3', '-smt2', '-in'], stdin=subprocess.PIPE,
-            stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
-
-else:
-    assert False
-
-def yices_write(stmt):
-    stmt = stmt.strip()
-    if debug_print:
-        print("> %s" % stmt)
-    if debug_file:
-        print(stmt, file=debug_file)
-        debug_file.flush()
-    yices.stdin.write(bytes(stmt + "\n", "ascii"))
-    yices.stdin.flush()
-
-def yices_read():
-    stmt = []
-    count_brackets = 0
-
-    while True:
-        line = yices.stdout.readline().decode("ascii").strip()
-        count_brackets += line.count("(")
-        count_brackets -= line.count(")")
-        stmt.append(line)
-        if debug_print:
-            print("< %s" % line)
-        if count_brackets == 0:
-            break
-        if not yices.poll():
-            print("Yices terminated unexpectedly: %s" % "".join(stmt))
-            sys.exit(1)
-
-    stmt = "".join(stmt)
-    if stmt.startswith("(error"):
-        print("Yices Error: %s" % stmt, file=sys.stderr)
-        sys.exit(1)
-
-    return stmt
-
-def yices_parse(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 yices_bv2hex(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 yices_bv2bin(v):
-    if v == "true": return "1"
-    if v == "false": return "0"
-    return v[2:]
-
-def yices_get(expr):
-    yices_write("(get-value (%s))" % (expr))
-    return yices_parse(yices_read())[0][1]
-
-def yices_get_net(mod_name, net_name, state_name):
-    return yices_get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
-
-def yices_get_net_bool(mod_name, net_name, state_name):
-    v = yices_get_net(mod_name, net_name, state_name)
-    assert v in ["true", "false"]
-    return 1 if v == "true" else 0
-
-def yices_get_net_hex(mod_name, net_name, state_name):
-    return yices_bv2hex(yices_get_net(mod_name, net_name, state_name))
-
-def yices_get_net_bin(mod_name, net_name, state_name):
-    return yices_bv2bin(yices_get_net(mod_name, net_name, state_name))
-
-
-# Main Program
-#####################################
-
 start_time = time()
+smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file)
 
 def timestamp():
     secs = int(time() - start_time)
     return "+ %6d [%3d:%02d:%02d] " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
 
-yices_write("(set-logic QF_AUFBV)")
+smt.write("(set-logic QF_AUFBV)")
 
 regs_a = list()
 regs_b = list()
@@ -153,7 +33,7 @@ with open("mem_equiv_a.smt2", "r") as f:
             line = line.split()
             regs_a.append((line[2], int(line[3])))
         else:
-            yices_write(line)
+            smt.write(line)
 
 with open("mem_equiv_b.smt2", "r") as f:
     for line in f:
@@ -161,139 +41,144 @@ with open("mem_equiv_b.smt2", "r") as f:
             line = line.split()
             regs_b.append((line[2], int(line[3])))
         else:
-            yices_write(line)
+            smt.write(line)
 
 for step in range(steps):
-    yices_write("(declare-fun a%d () main_a_s)" % step)
-    yices_write("(declare-fun b%d () main_b_s)" % step)
+    smt.write("(declare-fun a%d () main_a_s)" % step)
+    smt.write("(declare-fun b%d () main_b_s)" % step)
 
     if fastmem:
-        yices_write("(assert (|main_a_n domem| a%d))" % step)
-        yices_write("(assert (|main_b_n domem| b%d))" % step)
+        smt.write("(assert (|main_a_n domem| a%d))" % step)
+        smt.write("(assert (|main_b_n domem| b%d))" % step)
 
     if words > 0:
         if allmem:
-            yices_write("(assert (bvult (|main_a_n mem_addr| a%d) #x%08x))" % (step, words))
-            yices_write("(assert (bvult (|main_b_n mem_addr| b%d) #x%08x))" % (step, words))
+            smt.write("(assert (bvult (|main_a_n mem_addr| a%d) #x%08x))" % (step, words))
+            smt.write("(assert (bvult (|main_b_n mem_addr| b%d) #x%08x))" % (step, words))
         else:
-            yices_write("(assert (or (not (|main_a_n mem_valid| a%d)) (bvult (|main_a_n mem_addr| a%d) #x%08x)))" % (step, step, words))
-            yices_write("(assert (or (not (|main_b_n mem_valid| b%d)) (bvult (|main_b_n mem_addr| b%d) #x%08x)))" % (step, step, words))
-
-    # reset in first cycle
-    if step < 1:
-        yices_write("(assert (not (|main_a_n resetn| a%d)))" % step)
-        yices_write("(assert (not (|main_b_n resetn| b%d)))" % step)
-
-    else:
-        yices_write("(assert (|main_a_n resetn| a%d))" % step)
-        yices_write("(assert (|main_b_n resetn| b%d))" % step)
+            smt.write("(assert (or (not (|main_a_n mem_valid| a%d)) (bvult (|main_a_n mem_addr| a%d) #x%08x)))" % (step, step, words))
+            smt.write("(assert (or (not (|main_b_n mem_valid| b%d)) (bvult (|main_b_n mem_addr| b%d) #x%08x)))" % (step, step, words))
 
     if step == 0:
         # start with synced memory and register file
-        yices_write("(assert (= (|main_a_m cpu.cpuregs| a0) (|main_b_m cpu.cpuregs| b0)))")
-        yices_write("(assert (= (|main_a_m memory| a0) (|main_b_m memory| b0)))")
+        smt.write("(assert (= (|main_a_m cpu.cpuregs| a0) (|main_b_m cpu.cpuregs| b0)))")
+        smt.write("(assert (= (|main_a_m memory| a0) (|main_b_m memory| b0)))")
+
+        # reset in first cycle
+        smt.write("(assert (not (|main_a_n resetn| a%d)))" % step)
+        smt.write("(assert (not (|main_b_n resetn| b%d)))" % step)
 
     else:
-        yices_write("(assert (main_a_t a%d a%d))" % (step-1, step))
-        yices_write("(assert (main_b_t b%d b%d))" % (step-1, step))
+        smt.write("(assert (main_a_t a%d a%d))" % (step-1, step))
+        smt.write("(assert (main_b_t b%d b%d))" % (step-1, step))
+
+        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))
-        yices_write("(push 1)")
+        smt.write("(push 1)")
 
         # stop with a trap and no pending memory xfer
-        yices_write("(assert (not (|main_a_n mem_valid| a%d)))" % step)
-        yices_write("(assert (not (|main_b_n mem_valid| b%d)))" % step)
-        yices_write("(assert (|main_a_n trap| a%d))" % step)
-        yices_write("(assert (|main_b_n trap| b%d))" % step)
-
-        # look for differences in memory or register file
-        yices_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))))") % (step, step, step, step))
+        smt.write("(assert (not (|main_a_n mem_valid| a%d)))" % step)
+        smt.write("(assert (not (|main_b_n mem_valid| b%d)))" % step)
+        smt.write("(assert (|main_a_n trap| a%d))" % step)
+        smt.write("(assert (|main_b_n trap| b%d))" % step)
+
+        # look for differences in memory and/or register file
+        if check_mem and check_regs:
+            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))))") % (step, step, step, step))
+        elif check_mem:
+            smt.write(("(assert (distinct (|main_a_m memory| a%d) (|main_b_m memory| b%d)))") % (step, step))
+        elif check_regs:
+            smt.write(("(assert (distinct (|main_a_m cpu.cpuregs| a%d) (|main_b_m cpu.cpuregs| b%d)))") % (step, step))
+        else:
+            assert False
 
-        yices_write("(check-sat)")
+        smt.write("(check-sat)")
 
-        if yices_read() == "sat":
+        if smt.read() == "sat":
 
             print("%s Creating model.." % timestamp())
 
             def make_cpu_regs(step):
                 for i in range(1, 32):
-                    yices_write("(define-fun a%d_r%d () (_ BitVec 32) (select (|main_a_m cpu.cpuregs| a%d) #b%s))" % (step, i, step, bin(32+i)[3:]))
-                    yices_write("(define-fun b%d_r%d () (_ BitVec 32) (select (|main_b_m cpu.cpuregs| b%d) #b%s))" % (step, i, step, bin(32+i)[3:]))
+                    smt.write("(define-fun a%d_r%d () (_ BitVec 32) (select (|main_a_m cpu.cpuregs| a%d) #b%s))" % (step, i, step, bin(32+i)[3:]))
+                    smt.write("(define-fun b%d_r%d () (_ BitVec 32) (select (|main_b_m cpu.cpuregs| b%d) #b%s))" % (step, i, step, bin(32+i)[3:]))
 
             make_cpu_regs(0)
             make_cpu_regs(step)
 
-            yices_write("(check-sat)")
+            smt.write("(check-sat)")
 
             def print_status(mod, step):
-                resetn = yices_get_net_bool("main_" + mod, "resetn", "%s%d" % (mod, step))
-                memvld = yices_get_net_bool("main_" + mod, "mem_valid", "%s%d" % (mod, step))
-                domem  = yices_get_net_bool("main_" + mod, "domem", "%s%d" % (mod, step))
-                memrdy = yices_get_net_bool("main_" + mod, "mem_ready", "%s%d" % (mod, step))
-                trap   = yices_get_net_bool("main_" + mod, "trap", "%s%d" % (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))
+                domem  = smt.get_net_bool("main_" + mod, "domem", "%s%d" % (mod, step))
+                memrdy = smt.get_net_bool("main_" + mod, "mem_ready", "%s%d" % (mod, step))
+                trap   = smt.get_net_bool("main_" + mod, "trap", "%s%d" % (mod, step))
                 print("status %5s: resetn=%s, memvld=%s, domem=%s, memrdy=%s, trap=%s" % ("%s[%d]" % (mod, step), resetn, memvld, domem, memrdy, trap))
 
             def print_mem_xfer(mod, step):
-                if allmem or yices_get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, step, mod, mod, step)) == 'true':
-                    mem_addr = yices_get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, step))
-                    mem_wdata = yices_get_net_hex("main_" + mod, "mem_wdata", "%s%d" % (mod, step))
-                    mem_wstrb = yices_get_net_bin("main_" + mod, "mem_wstrb", "%s%d" % (mod, step))
-                    mem_rdata = yices_get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, step))
-                    if allmem and yices_get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, step, mod, mod, step)) == 'true':
+                if allmem or smt.get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, step, mod, mod, step)) == 'true':
+                    mem_addr = smt.get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, step))
+                    mem_wdata = smt.get_net_hex("main_" + mod, "mem_wdata", "%s%d" % (mod, step))
+                    mem_wstrb = smt.get_net_bin("main_" + mod, "mem_wstrb", "%s%d" % (mod, step))
+                    mem_rdata = smt.get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, step))
+                    if allmem and smt.get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, step, mod, mod, step)) == 'true':
                         print("mem %5s: addr=%s, wdata=%s, wstrb=%s, rdata=%s <-" % ("%s[%d]" % (mod, step), mem_addr, mem_wdata, mem_wstrb, mem_rdata))
                     else:
                         print("mem %5s: addr=%s, wdata=%s, wstrb=%s, rdata=%s" % ("%s[%d]" % (mod, step), mem_addr, mem_wdata, mem_wstrb, mem_rdata))
 
             def print_cpu_regs(step):
                 for i in range(1, 32):
-                    ra = yices_bv2hex(yices_get("a%d_r%d" % (step, i)))
-                    rb = yices_bv2hex(yices_get("b%d_r%d" % (step, i)))
+                    ra = smt.bv2hex(smt.get("a%d_r%d" % (step, i)))
+                    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 yices_read() == "sat"
+            assert smt.read() == "sat"
 
             if initzero:
                 for rn, rs in regs_a:
                     force_to_zero = True
-                    if yices_get_net_bin("main_a", rn, "a0").count("1") != 0:
+                    if smt.get_net_bin("main_a", rn, "a0").count("1") != 0:
                         print("Looking for a solution with |main_a_n %s| initialized to all zeros.." % rn)
-                        yices_write("(push 1)")
+                        smt.write("(push 1)")
                         if rs == 1:
-                            yices_write("(assert (not (|main_a_n %s| a0)))" % rn)
+                            smt.write("(assert (not (|main_a_n %s| a0)))" % rn)
                         else:
-                            yices_write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs))
-                        yices_write("(check-sat)")
-                        if yices_read() != "sat":
+                            smt.write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs))
+                        smt.write("(check-sat)")
+                        if smt.read() != "sat":
                             force_to_zero = False
-                        yices_write("(pop 1)")
+                        smt.write("(pop 1)")
                     if force_to_zero:
                         if rs == 1:
-                            yices_write("(assert (not (|main_a_n %s| a0)))" % rn)
+                            smt.write("(assert (not (|main_a_n %s| a0)))" % rn)
                         else:
-                            yices_write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs))
-                    yices_write("(check-sat)")
-                    assert yices_read() == "sat"
+                            smt.write("(assert (= (|main_a_n %s| a0) #b%s))" % (rn, "0" * rs))
+                    smt.write("(check-sat)")
+                    assert smt.read() == "sat"
                 for rn, rs in regs_b:
                     force_to_zero = True
-                    if yices_get_net_bin("main_b", rn, "b0").count("1") != 0:
+                    if smt.get_net_bin("main_b", rn, "b0").count("1") != 0:
                         print("Looking for a solution with |main_b_n %s| initialized to all zeros.." % rn)
-                        yices_write("(push 1)")
+                        smt.write("(push 1)")
                         if rs == 1:
-                            yices_write("(assert (not (|main_b_n %s| b0)))" % rn)
+                            smt.write("(assert (not (|main_b_n %s| b0)))" % rn)
                         else:
-                            yices_write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs))
-                        yices_write("(check-sat)")
-                        if yices_read() != "sat":
+                            smt.write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs))
+                        smt.write("(check-sat)")
+                        if smt.read() != "sat":
                             force_to_zero = False
-                        yices_write("(pop 1)")
+                        smt.write("(pop 1)")
                     if force_to_zero:
                         if rs == 1:
-                            yices_write("(assert (not (|main_b_n %s| b0)))" % rn)
+                            smt.write("(assert (not (|main_b_n %s| b0)))" % rn)
                         else:
-                            yices_write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs))
-                    yices_write("(check-sat)")
-                    assert yices_read() == "sat"
+                            smt.write("(assert (= (|main_b_n %s| b0) #b%s))" % (rn, "0" * rs))
+                    smt.write("(check-sat)")
+                    assert smt.read() == "sat"
 
             print()
             print_cpu_regs(0)
@@ -325,9 +210,9 @@ for step in range(steps):
                 memory_datas = { "a": dict(), "b": dict() }
                 for i in range(step, 0, -1):
                     for mod in ["a", "b"]:
-                        if allmem or yices_get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, i, mod, mod, i)) == 'true':
-                            mem_addr = yices_get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, i))
-                            mem_rdata = yices_get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, i))
+                        if allmem or smt.get("(and (|main_%s_n mem_valid| %s%d) (|main_%s_n mem_ready| %s%d))" % (mod, mod, i, mod, mod, i)) == 'true':
+                            mem_addr = smt.get_net_hex("main_" + mod, "mem_addr", "%s%d" % (mod, i))
+                            mem_rdata = smt.get_net_hex("main_" + mod, "mem_rdata", "%s%d" % (mod, i))
                             memory_datas[mod][mem_addr] = mem_rdata
                             memory_words = max((int(mem_addr, 16) >> 2)+1, memory_words)
                 memory_data = dict()
@@ -386,16 +271,16 @@ for step in range(steps):
                 print("", file=f)
 
                 for rn, rs in regs_a:
-                    print("        main_a.%s = %d'b %s;" % (rn, rs, yices_get_net_bin("main_a", rn, "a0")), file=f)
+                    print("        main_a.%s = %d'b %s;" % (rn, rs, smt.get_net_bin("main_a", rn, "a0")), file=f)
                 print("", file=f)
 
                 for rn, rs in regs_b:
-                    print("        main_b.%s = %d'b %s;" % (rn, rs, yices_get_net_bin("main_b", rn, "b0")), file=f)
+                    print("        main_b.%s = %d'b %s;" % (rn, rs, smt.get_net_bin("main_b", rn, "b0")), file=f)
                 print("", file=f)
 
                 for i in range(1, 32):
-                    ra = yices_bv2hex(yices_get("a%d_r%d" % (0, i)))
-                    rb = yices_bv2hex(yices_get("b%d_r%d" % (0, i)))
+                    ra = smt.bv2hex(smt.get("a%d_r%d" % (0, i)))
+                    rb = smt.bv2hex(smt.get("b%d_r%d" % (0, i)))
                     print("        main_a.cpu.cpuregs[%2d] = 'h %s;  main_b.cpu.cpuregs[%2d] = 'h %s;" % (i, ra, i, rb), file=f)
                 print("", file=f)
 
@@ -405,9 +290,9 @@ for step in range(steps):
                 print("", file=f)
 
                 for i in range(step+1):
-                    print("        resetn = %d;" % yices_get_net_bool("main_a", "resetn", "a%d" % i), file=f)
-                    print("        domem_a = %d;" % yices_get_net_bool("main_a", "domem", "a%d" % i), file=f)
-                    print("        domem_b = %d;" % yices_get_net_bool("main_b", "domem", "b%d" % i), file=f)
+                    print("        resetn = %d;" % smt.get_net_bool("main_a", "resetn", "a%d" % i), file=f)
+                    print("        domem_a = %d;" % smt.get_net_bool("main_a", "domem", "a%d" % i), file=f)
+                    print("        domem_b = %d;" % smt.get_net_bool("main_b", "domem", "b%d" % i), file=f)
                     print("        @(posedge clk);", file=f)
                 print("", file=f)
 
@@ -430,9 +315,9 @@ for step in range(steps):
             break
 
         else: # unsat
-            yices_write("(pop 1)")
+            smt.write("(pop 1)")
 
 print("%s Done." % timestamp())
-yices_write("(exit)")
-yices.wait()
+smt.write("(exit)")
+smt.wait()
 
diff --git a/scripts/smt2-bmc/smtio.py b/scripts/smt2-bmc/smtio.py
new file mode 100644
index 0000000..d9f165c
--- /dev/null
+++ b/scripts/smt2-bmc/smtio.py
@@ -0,0 +1,124 @@
+#!/usr/bin/python3
+
+import sys
+import subprocess
+
+class smtio:
+    def __init__(self, solver="yices", debug_print=False, debug_file=None):
+        if solver == "yices":
+            popen_vargs = ['yices-smt2', '--incremental']
+
+        if solver == "z3":
+            popen_vargs = ['z3', '-smt2', '-in']
+
+        self.debug_print = debug_print
+        self.debug_file = debug_file
+        self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+
+    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 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()
+