mirror of https://github.com/YosysHQ/picorv32.git
Refactoring of scripts/smt2-bmc/
This commit is contained in:
Clifford Wolf
parent
0ab0b6eca4
commit
b28e82cb81
|
|
@ -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()
|
||||
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
||||
Loading…
Reference in New Issue