yosys/backends/smt2/smtio.py

1077 lines
37 KiB
Python
Raw Normal View History

2015-10-13 18:31:54 -05:00
#
# yosys -- Yosys Open SYnthesis Suite
#
# Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
#
# Permission to use, copy, modify, and/or distribute this software for any
# purpose with or without fee is hereby granted, provided that the above
# copyright notice and this permission notice appear in all copies.
#
# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
2015-10-13 10:17:23 -05:00
import sys, re, os, signal
import subprocess
if os.name == "posix":
import resource
2016-09-07 13:57:56 -05:00
from copy import deepcopy
2015-10-13 10:17:23 -05:00
from select import select
from time import time
from queue import Queue, Empty
from threading import Thread
2015-10-13 10:17:23 -05:00
2016-09-02 05:09:09 -05:00
# This is needed so that the recursive SMT2 S-expression parser
# does not run out of stack frames when parsing large expressions
if os.name == "posix":
smtio_reclimit = 64 * 1024
if sys.getrecursionlimit() < smtio_reclimit:
sys.setrecursionlimit(smtio_reclimit)
current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK)
if current_rlimit_stack[0] != resource.RLIM_INFINITY:
smtio_stacksize = 128 * 1024 * 1024
if os.uname().sysname == "Darwin":
# MacOS has rather conservative stack limits
smtio_stacksize = 16 * 1024 * 1024
if current_rlimit_stack[1] != resource.RLIM_INFINITY:
smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
if current_rlimit_stack[0] < smtio_stacksize:
resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
# currently running solvers (so we can kill them)
running_solvers = dict()
forced_shutdown = False
solvers_index = 0
def force_shutdown(signum, frame):
global forced_shutdown
if not forced_shutdown:
forced_shutdown = True
if signum is not None:
print("<%s>" % signal.Signals(signum).name)
for p in running_solvers.values():
# os.killpg(os.getpgid(p.pid), signal.SIGTERM)
os.kill(p.pid, signal.SIGTERM)
sys.exit(1)
if os.name == "posix":
signal.signal(signal.SIGHUP, force_shutdown)
signal.signal(signal.SIGINT, force_shutdown)
signal.signal(signal.SIGTERM, force_shutdown)
def except_hook(exctype, value, traceback):
if not forced_shutdown:
sys.__excepthook__(exctype, value, traceback)
force_shutdown(None, None)
sys.excepthook = except_hook
hex_dict = {
"0": "0000", "1": "0001", "2": "0010", "3": "0011",
"4": "0100", "5": "0101", "6": "0110", "7": "0111",
"8": "1000", "9": "1001", "A": "1010", "B": "1011",
"C": "1100", "D": "1101", "E": "1110", "F": "1111",
"a": "1010", "b": "1011", "c": "1100", "d": "1101",
"e": "1110", "f": "1111"
}
2016-09-02 05:09:09 -05:00
class SmtModInfo:
def __init__(self):
self.inputs = set()
self.outputs = set()
self.registers = set()
2016-08-20 11:42:32 -05:00
self.memories = dict()
self.wires = set()
self.wsize = dict()
self.clocks = dict()
self.cells = dict()
self.asserts = dict()
self.covers = dict()
self.anyconsts = dict()
self.anyseqs = dict()
self.allconsts = dict()
self.allseqs = dict()
self.asize = dict()
2016-09-02 05:09:09 -05:00
class SmtIo:
def __init__(self, opts=None):
global solvers_index
self.logic = None
self.logic_qf = True
self.logic_ax = True
self.logic_uf = True
self.logic_bv = True
2017-03-20 06:00:35 -05:00
self.logic_dt = False
self.forall = False
2016-09-24 13:40:22 -05:00
self.produce_models = True
2016-10-03 13:30:38 -05:00
self.smt2cache = [list()]
self.p = None
self.p_index = solvers_index
solvers_index += 1
2015-10-13 10:17:23 -05:00
if opts is not None:
self.logic = opts.logic
2015-10-13 10:17:23 -05:00
self.solver = opts.solver
2017-02-19 15:51:29 -06:00
self.solver_opts = opts.solver_opts
2015-10-13 10:17:23 -05:00
self.debug_print = opts.debug_print
self.debug_file = opts.debug_file
self.dummy_file = opts.dummy_file
2015-10-13 10:17:23 -05:00
self.timeinfo = opts.timeinfo
2016-09-07 13:57:56 -05:00
self.unroll = opts.unroll
2016-10-03 13:30:38 -05:00
self.noincr = opts.noincr
2016-09-24 13:40:22 -05:00
self.info_stmts = opts.info_stmts
self.nocomments = opts.nocomments
2015-10-13 10:17:23 -05:00
else:
self.solver = "yices"
2017-02-19 15:51:29 -06:00
self.solver_opts = list()
2015-10-13 10:17:23 -05:00
self.debug_print = False
self.debug_file = None
self.dummy_file = None
self.timeinfo = os.name != "nt"
2016-09-07 13:57:56 -05:00
self.unroll = False
2016-10-03 13:30:38 -05:00
self.noincr = False
2016-09-24 13:40:22 -05:00
self.info_stmts = list()
self.nocomments = False
2015-10-13 10:17:23 -05:00
2017-03-20 06:00:35 -05:00
self.start_time = time()
self.modinfo = dict()
self.curmod = None
self.topmod = None
self.setup_done = False
def __del__(self):
if self.p is not None and not forced_shutdown:
os.killpg(os.getpgid(self.p.pid), signal.SIGTERM)
if running_solvers is not None:
del running_solvers[self.p_index]
2017-03-20 06:00:35 -05:00
def setup(self):
assert not self.setup_done
if self.forall:
self.unroll = False
2015-10-13 10:17:23 -05:00
if self.solver == "yices":
if self.noincr:
self.popen_vargs = ['yices-smt2'] + self.solver_opts
else:
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
2015-10-13 10:17:23 -05:00
if self.solver == "z3":
2017-02-19 15:51:29 -06:00
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
2015-10-13 10:17:23 -05:00
if self.solver == "cvc4":
if self.noincr:
self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
else:
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
2015-10-13 10:17:23 -05:00
if self.solver == "mathsat":
2017-02-19 15:51:29 -06:00
self.popen_vargs = ['mathsat'] + self.solver_opts
2015-10-13 10:17:23 -05:00
if self.solver == "boolector":
if self.noincr:
self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts
else:
self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
2016-09-07 13:57:56 -05:00
self.unroll = True
2016-10-01 06:54:21 -05:00
if self.solver == "abc":
2017-02-19 15:51:29 -06:00
if len(self.solver_opts) > 0:
self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]
else:
self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
2016-10-03 13:43:38 -05:00
self.logic_ax = False
2016-10-01 06:54:21 -05:00
self.unroll = True
2016-10-03 13:30:38 -05:00
self.noincr = True
2016-10-01 06:54:21 -05:00
if self.solver == "dummy":
assert self.dummy_file is not None
self.dummy_fd = open(self.dummy_file, "r")
else:
if self.dummy_file is not None:
self.dummy_fd = open(self.dummy_file, "w")
2016-10-03 13:30:38 -05:00
if not self.noincr:
2017-10-25 08:45:32 -05:00
self.p_open()
2017-05-08 07:33:22 -05:00
if self.unroll:
assert not self.forall
2017-05-08 07:33:22 -05:00
self.logic_uf = False
self.unroll_idcnt = 0
self.unroll_buffer = ""
self.unroll_sorts = set()
self.unroll_objs = set()
self.unroll_decls = dict()
self.unroll_cache = dict()
self.unroll_stack = list()
if self.logic is None:
self.logic = ""
if self.logic_qf: self.logic += "QF_"
if self.logic_ax: self.logic += "A"
if self.logic_uf: self.logic += "UF"
if self.logic_bv: self.logic += "BV"
if self.logic_dt: self.logic = "ALL"
self.setup_done = True
2016-09-24 13:40:22 -05:00
for stmt in self.info_stmts:
self.write(stmt)
2016-09-24 13:40:22 -05:00
if self.produce_models:
self.write("(set-option :produce-models true)")
self.write("(set-logic %s)" % self.logic)
2015-10-13 10:17:23 -05:00
def timestamp(self):
secs = int(time() - self.start_time)
return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)
2015-10-13 10:17:23 -05:00
2016-09-07 13:57:56 -05:00
def replace_in_stmt(self, stmt, pat, repl):
if stmt == pat:
return repl
if isinstance(stmt, list):
return [self.replace_in_stmt(s, pat, repl) for s in stmt]
return stmt
def unroll_stmt(self, stmt):
if not isinstance(stmt, list):
return stmt
stmt = [self.unroll_stmt(s) for s in stmt]
if len(stmt) >= 2 and not isinstance(stmt[0], list) and stmt[0] in self.unroll_decls:
assert stmt[1] in self.unroll_objs
key = tuple(stmt)
if key not in self.unroll_cache:
decl = deepcopy(self.unroll_decls[key[0]])
self.unroll_cache[key] = "|UNROLL#%d|" % self.unroll_idcnt
decl[1] = self.unroll_cache[key]
self.unroll_idcnt += 1
if decl[0] == "declare-fun":
if isinstance(decl[3], list) or decl[3] not in self.unroll_sorts:
self.unroll_objs.add(decl[1])
decl[2] = list()
else:
self.unroll_objs.add(decl[1])
decl = list()
elif decl[0] == "define-fun":
arg_index = 1
for arg_name, arg_sort in decl[2]:
decl[4] = self.replace_in_stmt(decl[4], arg_name, key[arg_index])
arg_index += 1
decl[2] = list()
if len(decl) > 0:
decl = self.unroll_stmt(decl)
self.write(self.unparse(decl), unroll=False)
return self.unroll_cache[key]
return stmt
def p_thread_main(self):
while True:
data = self.p.stdout.readline().decode("ascii")
if data == "": break
self.p_queue.put(data)
self.p_queue.put("")
self.p_running = False
2017-10-25 08:45:32 -05:00
def p_open(self):
assert self.p is None
2017-10-25 08:45:32 -05:00
self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
running_solvers[self.p_index] = self.p
self.p_running = True
self.p_next = None
self.p_queue = Queue()
self.p_thread = Thread(target=self.p_thread_main)
self.p_thread.start()
2017-10-25 08:45:32 -05:00
def p_write(self, data, flush):
assert self.p is not None
self.p.stdin.write(bytes(data, "ascii"))
if flush: self.p.stdin.flush()
def p_read(self):
assert self.p is not None
if self.p_next is not None:
data = self.p_next
self.p_next = None
return data
if not self.p_running:
return ""
return self.p_queue.get()
def p_poll(self, timeout=0.1):
assert self.p is not None
assert self.p_running
if self.p_next is not None:
return False
try:
self.p_next = self.p_queue.get(True, timeout)
return False
except Empty:
return True
2017-10-25 08:45:32 -05:00
def p_close(self):
assert self.p is not None
2017-10-25 08:45:32 -05:00
self.p.stdin.close()
self.p_thread.join()
assert not self.p_running
del running_solvers[self.p_index]
2017-10-25 08:45:32 -05:00
self.p = None
self.p_next = None
self.p_queue = None
self.p_thread = None
2017-10-25 08:45:32 -05:00
2016-09-07 13:57:56 -05:00
def write(self, stmt, unroll=True):
if stmt.startswith(";"):
self.info(stmt)
2017-03-20 06:00:35 -05:00
if not self.setup_done:
self.info_stmts.append(stmt)
return
elif not self.setup_done:
self.setup()
2015-10-13 10:17:23 -05:00
stmt = stmt.strip()
2016-09-24 13:40:22 -05:00
if self.nocomments or self.unroll:
2017-02-26 07:39:07 -06:00
stmt = re.sub(r" *;.*", "", stmt)
if stmt == "": return
2016-09-24 13:40:22 -05:00
if unroll and self.unroll:
2016-09-07 13:57:56 -05:00
stmt = self.unroll_buffer + stmt
self.unroll_buffer = ""
s = re.sub(r"\|[^|]*\|", "", stmt)
if s.count("(") != s.count(")"):
self.unroll_buffer = stmt + " "
return
s = self.parse(stmt)
if self.debug_print:
print("-> %s" % s)
if len(s) == 3 and s[0] == "declare-sort" and s[2] == "0":
self.unroll_sorts.add(s[1])
return
elif len(s) == 4 and s[0] == "declare-fun" and s[2] == [] and s[3] in self.unroll_sorts:
self.unroll_objs.add(s[1])
return
elif len(s) >= 4 and s[0] == "declare-fun":
for arg_sort in s[2]:
if arg_sort in self.unroll_sorts:
self.unroll_decls[s[1]] = s
return
elif len(s) >= 4 and s[0] == "define-fun":
for arg_name, arg_sort in s[2]:
if arg_sort in self.unroll_sorts:
self.unroll_decls[s[1]] = s
return
stmt = self.unparse(self.unroll_stmt(s))
if stmt == "(push 1)":
self.unroll_stack.append((
deepcopy(self.unroll_sorts),
deepcopy(self.unroll_objs),
deepcopy(self.unroll_decls),
deepcopy(self.unroll_cache),
))
if stmt == "(pop 1)":
self.unroll_sorts, self.unroll_objs, self.unroll_decls, self.unroll_cache = self.unroll_stack.pop()
2015-10-13 10:17:23 -05:00
if self.debug_print:
print("> %s" % stmt)
2015-10-13 10:17:23 -05:00
if self.debug_file:
print(stmt, file=self.debug_file)
self.debug_file.flush()
if self.solver != "dummy":
2016-10-03 13:30:38 -05:00
if self.noincr:
2016-10-03 17:54:44 -05:00
if self.p is not None and not stmt.startswith("(get-"):
2017-10-25 08:45:32 -05:00
self.p_close()
2016-10-03 13:30:38 -05:00
if stmt == "(push 1)":
self.smt2cache.append(list())
elif stmt == "(pop 1)":
self.smt2cache.pop()
else:
2016-10-03 17:54:44 -05:00
if self.p is not None:
2017-10-25 08:45:32 -05:00
self.p_write(stmt + "\n", True)
2016-10-03 13:30:38 -05:00
self.smt2cache[-1].append(stmt)
else:
2017-10-25 08:45:32 -05:00
self.p_write(stmt + "\n", True)
2015-10-13 10:17:23 -05:00
def info(self, stmt):
if not stmt.startswith("; yosys-smt2-"):
return
fields = stmt.split()
if fields[1] == "yosys-smt2-nomem":
if self.logic is None:
self.logic_ax = False
if fields[1] == "yosys-smt2-nobv":
if self.logic is None:
self.logic_bv = False
2017-03-20 06:00:35 -05:00
if fields[1] == "yosys-smt2-stdt":
if self.logic is None:
self.logic_dt = True
if fields[1] == "yosys-smt2-forall":
if self.logic is None:
self.logic_qf = False
self.forall = True
if fields[1] == "yosys-smt2-module":
self.curmod = fields[2]
2016-09-02 05:09:09 -05:00
self.modinfo[self.curmod] = SmtModInfo()
if fields[1] == "yosys-smt2-cell":
self.modinfo[self.curmod].cells[fields[3]] = fields[2]
if fields[1] == "yosys-smt2-topmod":
self.topmod = fields[2]
if fields[1] == "yosys-smt2-input":
self.modinfo[self.curmod].inputs.add(fields[2])
self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
if fields[1] == "yosys-smt2-output":
self.modinfo[self.curmod].outputs.add(fields[2])
self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
if fields[1] == "yosys-smt2-register":
self.modinfo[self.curmod].registers.add(fields[2])
self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
2016-08-20 11:42:32 -05:00
if fields[1] == "yosys-smt2-memory":
self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5]), int(fields[6]), fields[7] == "async")
2016-08-20 11:42:32 -05:00
if fields[1] == "yosys-smt2-wire":
self.modinfo[self.curmod].wires.add(fields[2])
self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
if fields[1] == "yosys-smt2-clock":
for edge in fields[3:]:
if fields[2] not in self.modinfo[self.curmod].clocks:
self.modinfo[self.curmod].clocks[fields[2]] = edge
elif self.modinfo[self.curmod].clocks[fields[2]] != edge:
self.modinfo[self.curmod].clocks[fields[2]] = "event"
if fields[1] == "yosys-smt2-assert":
self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
if fields[1] == "yosys-smt2-cover":
self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
if fields[1] == "yosys-smt2-anyconst":
self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
if fields[1] == "yosys-smt2-anyseq":
self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
if fields[1] == "yosys-smt2-allconst":
self.modinfo[self.curmod].allconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
if fields[1] == "yosys-smt2-allseq":
self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
2016-08-20 11:42:32 -05:00
def hiernets(self, top, regs_only=False):
def hiernets_worker(nets, mod, cursor):
for netname in sorted(self.modinfo[mod].wsize.keys()):
2016-08-20 11:42:32 -05:00
if not regs_only or netname in self.modinfo[mod].registers:
nets.append(cursor + [netname])
for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
hiernets_worker(nets, celltype, cursor + [cellname])
nets = list()
hiernets_worker(nets, top, [])
return nets
def hieranyconsts(self, top):
def worker(results, mod, cursor):
for name, value in sorted(self.modinfo[mod].anyconsts.items()):
width = self.modinfo[mod].asize[name]
results.append((cursor, name, value[0], value[1], width))
for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
worker(results, celltype, cursor + [cellname])
results = list()
worker(results, top, [])
return results
def hieranyseqs(self, top):
def worker(results, mod, cursor):
for name, value in sorted(self.modinfo[mod].anyseqs.items()):
width = self.modinfo[mod].asize[name]
results.append((cursor, name, value[0], value[1], width))
for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
worker(results, celltype, cursor + [cellname])
results = list()
worker(results, top, [])
return results
def hierallconsts(self, top):
def worker(results, mod, cursor):
for name, value in sorted(self.modinfo[mod].allconsts.items()):
width = self.modinfo[mod].asize[name]
results.append((cursor, name, value[0], value[1], width))
for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
worker(results, celltype, cursor + [cellname])
results = list()
worker(results, top, [])
return results
def hierallseqs(self, top):
def worker(results, mod, cursor):
for name, value in sorted(self.modinfo[mod].allseqs.items()):
width = self.modinfo[mod].asize[name]
results.append((cursor, name, value[0], value[1], width))
for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
worker(results, celltype, cursor + [cellname])
results = list()
worker(results, top, [])
return results
2016-08-20 11:42:32 -05:00
def hiermems(self, top):
def hiermems_worker(mems, mod, cursor):
for memname in sorted(self.modinfo[mod].memories.keys()):
mems.append(cursor + [memname])
for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
hiermems_worker(mems, celltype, cursor + [cellname])
mems = list()
hiermems_worker(mems, top, [])
return mems
2015-10-13 10:17:23 -05:00
def read(self):
stmt = []
count_brackets = 0
while True:
if self.solver == "dummy":
line = self.dummy_fd.readline().strip()
else:
line = self.p_read().strip()
if self.dummy_file is not None:
self.dummy_fd.write(line + "\n")
2015-10-13 10:17:23 -05:00
count_brackets += line.count("(")
count_brackets -= line.count(")")
stmt.append(line)
2015-10-13 10:17:23 -05:00
if self.debug_print:
print("< %s" % line)
if count_brackets == 0:
break
if self.solver != "dummy" and self.p.poll():
print("%s Solver terminated unexpectedly: %s" % (self.timestamp(), "".join(stmt)), flush=True)
2015-10-13 10:17:23 -05:00
sys.exit(1)
stmt = "".join(stmt)
if stmt.startswith("(error"):
print("%s Solver Error: %s" % (self.timestamp(), stmt), flush=True)
if self.solver != "dummy":
self.p_close()
2015-10-13 10:17:23 -05:00
sys.exit(1)
return stmt
def check_sat(self):
if self.debug_print:
print("> (check-sat)")
2016-09-24 13:40:22 -05:00
if self.debug_file and not self.nocomments:
2015-10-13 10:17:23 -05:00
print("; running check-sat..", file=self.debug_file)
self.debug_file.flush()
if self.solver != "dummy":
2016-10-03 13:30:38 -05:00
if self.noincr:
if self.p is not None:
2017-10-25 08:45:32 -05:00
self.p_close()
self.p_open()
2016-10-03 13:30:38 -05:00
for cache_ctx in self.smt2cache:
for cache_stmt in cache_ctx:
2017-10-25 08:45:32 -05:00
self.p_write(cache_stmt + "\n", False)
2016-10-03 13:30:38 -05:00
2017-10-25 08:45:32 -05:00
self.p_write("(check-sat)\n", True)
2015-10-13 10:17:23 -05:00
if self.timeinfo:
i = 0
s = "/-\|"
2015-10-13 10:17:23 -05:00
count = 0
num_bs = 0
while self.p_poll():
count += 1
2015-10-13 10:17:23 -05:00
if count < 25:
continue
2015-10-13 10:17:23 -05:00
if count % 10 == 0 or count == 25:
secs = count // 10
2015-10-13 10:17:23 -05:00
if secs < 60:
m = "(%d seconds)" % secs
elif secs < 60*60:
m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
else:
m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
2015-10-13 10:17:23 -05:00
print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
num_bs = len(m) + 3
2015-10-13 10:17:23 -05:00
else:
print("\b" + s[i], end="", file=sys.stderr)
2015-10-13 10:17:23 -05:00
sys.stderr.flush()
i = (i + 1) % len(s)
2015-10-13 10:17:23 -05:00
if num_bs != 0:
print("\b \b" * num_bs, end="", file=sys.stderr)
sys.stderr.flush()
2015-10-13 10:17:23 -05:00
else:
count = 0
while self.p_poll(60):
count += 1
msg = None
if count == 1:
msg = "1 minute"
elif count in [5, 10, 15, 30]:
msg = "%d minutes" % count
elif count == 60:
msg = "1 hour"
elif count % 60 == 0:
msg = "%d hours" % (count // 60)
if msg is not None:
print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)
2015-10-13 10:17:23 -05:00
result = self.read()
2015-10-13 10:17:23 -05:00
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()
if result not in ["sat", "unsat"]:
if result == "":
print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
else:
print("%s Unexpected response from solver: %s" % (self.timestamp(), result), flush=True)
if self.solver != "dummy":
self.p_close()
sys.exit(1)
2015-10-13 10:17:23 -05:00
return result
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]
2016-09-07 13:57:56 -05:00
def unparse(self, stmt):
if isinstance(stmt, list):
return "(" + " ".join([self.unparse(s) for s in stmt]) + ")"
return stmt
2015-10-13 10:17:23 -05:00
def bv2hex(self, v):
h = ""
2016-09-02 03:12:30 -05:00
v = self.bv2bin(v)
2015-10-14 16:23:25 -05:00
while len(v) > 0:
2015-10-13 10:17:23 -05:00
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 type(v) is list and len(v) == 3 and v[0] == "_" and v[1].startswith("bv"):
x, n = int(v[1][2:]), int(v[2])
return "".join("1" if (x & (1 << i)) else "0" for i in range(n-1, -1, -1))
2015-10-13 10:17:23 -05:00
if v == "true": return "1"
if v == "false": return "0"
2015-10-14 16:23:25 -05:00
if v.startswith("#b"):
return v[2:]
if v.startswith("#x"):
2016-09-02 04:50:23 -05:00
return "".join(hex_dict.get(x) for x in v[2:])
2015-10-14 16:23:25 -05:00
assert False
2015-10-13 10:17:23 -05:00
def bv2int(self, v):
return int(self.bv2bin(v), 2)
2015-10-13 10:17:23 -05:00
def get(self, expr):
self.write("(get-value (%s))" % (expr))
return self.parse(self.read())[0][1]
def get_list(self, expr_list):
2016-08-20 11:42:32 -05:00
if len(expr_list) == 0:
return []
self.write("(get-value (%s))" % " ".join(expr_list))
return [n[1] for n in self.parse(self.read())]
2016-08-22 10:27:43 -05:00
def get_path(self, mod, path):
assert mod in self.modinfo
path = path.split(".")
for i in range(len(path)-1):
first = ".".join(path[0:i+1])
second = ".".join(path[i+1:])
if first in self.modinfo[mod].cells:
nextmod = self.modinfo[mod].cells[first]
return [first] + self.get_path(nextmod, second)
return [".".join(path)]
def net_expr(self, mod, base, path):
if len(path) == 0:
return base
if len(path) == 1:
assert mod in self.modinfo
if path[0] == "":
return base
if path[0] in self.modinfo[mod].cells:
return "(|%s_h %s| %s)" % (mod, path[0], base)
2016-08-22 10:27:43 -05:00
if path[0] in self.modinfo[mod].wsize:
return "(|%s_n %s| %s)" % (mod, path[0], base)
if path[0] in self.modinfo[mod].memories:
return "(|%s_m %s| %s)" % (mod, path[0], base)
assert 0
assert mod in self.modinfo
assert path[0] in self.modinfo[mod].cells
nextmod = self.modinfo[mod].cells[path[0]]
nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
return self.net_expr(nextmod, nextbase, path[1:])
def net_width(self, mod, net_path):
for i in range(len(net_path)-1):
assert mod in self.modinfo
assert net_path[i] in self.modinfo[mod].cells
mod = self.modinfo[mod].cells[net_path[i]]
assert mod in self.modinfo
assert net_path[-1] in self.modinfo[mod].wsize
return self.modinfo[mod].wsize[net_path[-1]]
def net_clock(self, mod, net_path):
for i in range(len(net_path)-1):
assert mod in self.modinfo
assert net_path[i] in self.modinfo[mod].cells
mod = self.modinfo[mod].cells[net_path[i]]
assert mod in self.modinfo
if net_path[-1] not in self.modinfo[mod].clocks:
return None
return self.modinfo[mod].clocks[net_path[-1]]
def net_exists(self, mod, net_path):
for i in range(len(net_path)-1):
if mod not in self.modinfo: return False
if net_path[i] not in self.modinfo[mod].cells: return False
mod = self.modinfo[mod].cells[net_path[i]]
if mod not in self.modinfo: return False
if net_path[-1] not in self.modinfo[mod].wsize: return False
return True
def mem_exists(self, mod, mem_path):
for i in range(len(mem_path)-1):
if mod not in self.modinfo: return False
if mem_path[i] not in self.modinfo[mod].cells: return False
mod = self.modinfo[mod].cells[mem_path[i]]
if mod not in self.modinfo: return False
if mem_path[-1] not in self.modinfo[mod].memories: return False
return True
def mem_expr(self, mod, base, path, port=None, infomode=False):
2016-08-20 11:42:32 -05:00
if len(path) == 1:
assert mod in self.modinfo
assert path[0] in self.modinfo[mod].memories
if infomode:
return self.modinfo[mod].memories[path[0]]
return "(|%s_m%s %s| %s)" % (mod, "" if port is None else ":%s" % port, path[0], base)
2016-08-20 11:42:32 -05:00
assert mod in self.modinfo
assert path[0] in self.modinfo[mod].cells
nextmod = self.modinfo[mod].cells[path[0]]
nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
return self.mem_expr(nextmod, nextbase, path[1:], port=port, infomode=infomode)
2016-08-20 11:42:32 -05:00
def mem_info(self, mod, path):
return self.mem_expr(mod, "", path, infomode=True)
def get_net(self, mod_name, net_path, state_name):
return self.get(self.net_expr(mod_name, state_name, net_path))
2015-10-13 10:17:23 -05:00
def get_net_list(self, mod_name, net_path_list, state_name):
return self.get_list([self.net_expr(mod_name, state_name, n) for n in net_path_list])
2015-10-13 10:17:23 -05:00
def get_net_hex(self, mod_name, net_path, state_name):
return self.bv2hex(self.get_net(mod_name, net_path, state_name))
2015-10-13 10:17:23 -05:00
def get_net_hex_list(self, mod_name, net_path_list, state_name):
return [self.bv2hex(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
def get_net_bin(self, mod_name, net_path, state_name):
return self.bv2bin(self.get_net(mod_name, net_path, state_name))
2015-10-13 10:17:23 -05:00
def get_net_bin_list(self, mod_name, net_path_list, state_name):
return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
2015-10-13 10:17:23 -05:00
def wait(self):
2016-10-03 17:54:44 -05:00
if self.p is not None:
self.p.wait()
self.p_close()
2015-10-13 10:17:23 -05:00
class SmtOpts:
2015-10-13 10:17:23 -05:00
def __init__(self):
2017-02-19 15:51:29 -06:00
self.shortopts = "s:S:v"
2016-10-03 13:30:38 -05:00
self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.solver = "yices"
2017-02-19 15:51:29 -06:00
self.solver_opts = list()
2015-10-13 10:17:23 -05:00
self.debug_print = False
self.debug_file = None
self.dummy_file = None
2016-09-07 14:01:51 -05:00
self.unroll = False
2016-10-03 13:30:38 -05:00
self.noincr = False
self.timeinfo = os.name != "nt"
self.logic = None
2016-09-24 13:40:22 -05:00
self.info_stmts = list()
self.nocomments = False
2015-10-13 10:17:23 -05:00
def handle(self, o, a):
if o == "-s":
self.solver = a
2017-02-19 15:51:29 -06:00
elif o == "-S":
self.solver_opts.append(a)
2015-10-13 10:17:23 -05:00
elif o == "-v":
self.debug_print = True
2016-09-07 13:57:56 -05:00
elif o == "--unroll":
self.unroll = True
2016-10-03 13:30:38 -05:00
elif o == "--noincr":
self.noincr = True
2016-09-24 13:40:22 -05:00
elif o == "--noprogress":
2017-01-04 05:03:04 -06:00
self.timeinfo = False
2016-08-20 09:07:59 -05:00
elif o == "--dump-smt2":
2015-10-13 10:17:23 -05:00
self.debug_file = open(a, "w")
elif o == "--logic":
self.logic = a
elif o == "--dummy":
self.dummy_file = a
2016-09-24 13:40:22 -05:00
elif o == "--info":
self.info_stmts.append(a)
elif o == "--nocomments":
self.nocomments = True
2015-10-13 10:17:23 -05:00
else:
return False
return True
def helpmsg(self):
return """
-s <solver>
set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
default: yices
2015-10-13 10:17:23 -05:00
2017-02-19 15:51:29 -06:00
-S <opt>
pass <opt> as command line argument to the solver
--logic <smt2_logic>
use the specified SMT2 logic (e.g. QF_AUFBV)
--dummy <filename>
if solver is "dummy", read solver output from that file
otherwise: write solver output to that file
2015-10-13 10:17:23 -05:00
-v
enable debug output
2016-09-07 13:57:56 -05:00
--unroll
unroll uninterpreted functions
2016-10-03 13:30:38 -05:00
--noincr
don't use incremental solving, instead restart solver for
each (check-sat). This also avoids (push) and (pop).
2016-09-24 13:40:22 -05:00
--noprogress
2016-09-07 13:57:56 -05:00
disable timer display during solving
(this option is set implicitly on Windows)
2015-10-13 10:17:23 -05:00
2016-08-20 09:07:59 -05:00
--dump-smt2 <filename>
2015-10-13 10:17:23 -05:00
write smt2 statements to file
2016-09-24 13:40:22 -05:00
--info <smt2-info-stmt>
include the specified smt2 info statement in the smt2 output
--nocomments
strip all comments from the generated smt2 code
2015-10-13 10:17:23 -05:00
"""
class MkVcd:
2015-10-13 10:17:23 -05:00
def __init__(self, f):
self.f = f
self.t = -1
self.nets = dict()
self.clocks = dict()
2015-10-13 10:17:23 -05:00
def add_net(self, path, width):
path = tuple(path)
2015-10-13 10:17:23 -05:00
assert self.t == -1
key = "n%d" % len(self.nets)
self.nets[path] = (key, width)
2015-10-13 10:17:23 -05:00
def add_clock(self, path, edge):
path = tuple(path)
assert self.t == -1
key = "n%d" % len(self.nets)
self.nets[path] = (key, 1)
self.clocks[path] = (key, edge)
def set_net(self, path, bits):
path = tuple(path)
2015-10-13 10:17:23 -05:00
assert self.t >= 0
assert path in self.nets
if path not in self.clocks:
print("b%s %s" % (bits, self.nets[path][0]), file=self.f)
2015-10-13 10:17:23 -05:00
def escape_name(self, name):
name = re.sub(r"\[([0-9a-zA-Z_]*[a-zA-Z_][0-9a-zA-Z_]*)\]", r"<\1>", name)
if re.match("[\[\]]", name) and name[0] != "\\":
name = "\\" + name
return name
2015-10-13 10:17:23 -05:00
def set_time(self, t):
assert t >= self.t
if t != self.t:
if self.t == -1:
print("$var integer 32 t smt_step $end", file=self.f)
2015-10-15 08:08:41 -05:00
print("$var event 1 ! smt_clock $end", file=self.f)
scope = []
for path in sorted(self.nets):
key, width = self.nets[path]
uipath = list(path)
if "." in uipath[-1]:
uipath = uipath[0:-1] + uipath[-1].split(".")
for i in range(len(uipath)):
uipath[i] = re.sub(r"\[([^\]]*)\]", r"<\1>", uipath[i])
while uipath[:len(scope)] != scope:
print("$upscope $end", file=self.f)
scope = scope[:-1]
while uipath[:-1] != scope:
print("$scope module %s $end" % uipath[len(scope)], file=self.f)
scope.append(uipath[len(scope)])
if path in self.clocks and self.clocks[path][1] == "event":
print("$var event 1 %s %s $end" % (key, uipath[-1]), file=self.f)
else:
print("$var wire %d %s %s $end" % (width, key, uipath[-1]), file=self.f)
for i in range(len(scope)):
print("$upscope $end", file=self.f)
2015-10-13 10:17:23 -05:00
print("$enddefinitions $end", file=self.f)
2015-10-13 10:17:23 -05:00
self.t = t
assert self.t >= 0
if self.t > 0:
print("#%d" % (10 * self.t - 5), file=self.f)
for path in sorted(self.clocks.keys()):
if self.clocks[path][1] == "posedge":
print("b0 %s" % self.nets[path][0], file=self.f)
elif self.clocks[path][1] == "negedge":
print("b1 %s" % self.nets[path][0], file=self.f)
print("#%d" % (10 * self.t), file=self.f)
2015-10-15 08:08:41 -05:00
print("1!", file=self.f)
print("b%s t" % format(self.t, "032b"), file=self.f)
2015-10-13 10:17:23 -05:00
for path in sorted(self.clocks.keys()):
if self.clocks[path][1] == "negedge":
print("b0 %s" % self.nets[path][0], file=self.f)
else:
print("b1 %s" % self.nets[path][0], file=self.f)