From b28e82cb81ae81f648a14a930de9373ed9583e67 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 15 Aug 2015 00:20:06 +0200 Subject: [PATCH] Refactoring of scripts/smt2-bmc/ --- scripts/smt2-bmc/mem_equiv.py | 305 +++++++++++----------------------- scripts/smt2-bmc/smtio.py | 124 ++++++++++++++ 2 files changed, 219 insertions(+), 210 deletions(-) create mode 100644 scripts/smt2-bmc/smtio.py 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) + 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 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)) + # 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() +