mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 19:52:31 +00:00
1085 lines
37 KiB
Python
1085 lines
37 KiB
Python
#
|
|
# 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.
|
|
#
|
|
|
|
import sys, re, os, signal
|
|
import subprocess
|
|
if os.name == "posix":
|
|
import resource
|
|
from copy import deepcopy
|
|
from select import select
|
|
from time import time
|
|
from queue import Queue, Empty
|
|
from threading import Thread
|
|
|
|
|
|
# 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:
|
|
try:
|
|
resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
|
|
except ValueError:
|
|
# couldn't get more stack, just run with what we have
|
|
pass
|
|
|
|
|
|
# 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"
|
|
}
|
|
|
|
|
|
class SmtModInfo:
|
|
def __init__(self):
|
|
self.inputs = set()
|
|
self.outputs = set()
|
|
self.registers = set()
|
|
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()
|
|
|
|
|
|
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
|
|
self.logic_dt = False
|
|
self.forall = False
|
|
self.produce_models = True
|
|
self.smt2cache = [list()]
|
|
self.p = None
|
|
self.p_index = solvers_index
|
|
solvers_index += 1
|
|
|
|
if opts is not None:
|
|
self.logic = opts.logic
|
|
self.solver = opts.solver
|
|
self.solver_opts = opts.solver_opts
|
|
self.debug_print = opts.debug_print
|
|
self.debug_file = opts.debug_file
|
|
self.dummy_file = opts.dummy_file
|
|
self.timeinfo = opts.timeinfo
|
|
self.unroll = opts.unroll
|
|
self.noincr = opts.noincr
|
|
self.info_stmts = opts.info_stmts
|
|
self.nocomments = opts.nocomments
|
|
|
|
else:
|
|
self.solver = "yices"
|
|
self.solver_opts = list()
|
|
self.debug_print = False
|
|
self.debug_file = None
|
|
self.dummy_file = None
|
|
self.timeinfo = os.name != "nt"
|
|
self.unroll = False
|
|
self.noincr = False
|
|
self.info_stmts = list()
|
|
self.nocomments = False
|
|
|
|
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]
|
|
|
|
def setup(self):
|
|
assert not self.setup_done
|
|
|
|
if self.forall:
|
|
self.unroll = False
|
|
|
|
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
|
|
|
|
if self.solver == "z3":
|
|
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
|
|
|
|
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
|
|
|
|
if self.solver == "mathsat":
|
|
self.popen_vargs = ['mathsat'] + self.solver_opts
|
|
|
|
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
|
|
self.unroll = True
|
|
|
|
if self.solver == "abc":
|
|
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']
|
|
self.logic_ax = False
|
|
self.unroll = True
|
|
self.noincr = True
|
|
|
|
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")
|
|
if not self.noincr:
|
|
self.p_open()
|
|
|
|
if self.unroll:
|
|
assert not self.forall
|
|
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
|
|
|
|
for stmt in self.info_stmts:
|
|
self.write(stmt)
|
|
|
|
if self.produce_models:
|
|
self.write("(set-option :produce-models true)")
|
|
|
|
self.write("(set-logic %s)" % self.logic)
|
|
|
|
def timestamp(self):
|
|
secs = int(time() - self.start_time)
|
|
return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)
|
|
|
|
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
|
|
|
|
def p_open(self):
|
|
assert self.p is None
|
|
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()
|
|
|
|
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
|
|
|
|
def p_close(self):
|
|
assert self.p is not None
|
|
self.p.stdin.close()
|
|
self.p_thread.join()
|
|
assert not self.p_running
|
|
del running_solvers[self.p_index]
|
|
self.p = None
|
|
self.p_next = None
|
|
self.p_queue = None
|
|
self.p_thread = None
|
|
|
|
def write(self, stmt, unroll=True):
|
|
if stmt.startswith(";"):
|
|
self.info(stmt)
|
|
if not self.setup_done:
|
|
self.info_stmts.append(stmt)
|
|
return
|
|
elif not self.setup_done:
|
|
self.setup()
|
|
|
|
stmt = stmt.strip()
|
|
|
|
if self.nocomments or self.unroll:
|
|
stmt = re.sub(r" *;.*", "", stmt)
|
|
if stmt == "": return
|
|
|
|
if unroll and self.unroll:
|
|
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()
|
|
|
|
if self.debug_print:
|
|
print("> %s" % stmt)
|
|
|
|
if self.debug_file:
|
|
print(stmt, file=self.debug_file)
|
|
self.debug_file.flush()
|
|
|
|
if self.solver != "dummy":
|
|
if self.noincr:
|
|
if self.p is not None and not stmt.startswith("(get-"):
|
|
self.p_close()
|
|
if stmt == "(push 1)":
|
|
self.smt2cache.append(list())
|
|
elif stmt == "(pop 1)":
|
|
self.smt2cache.pop()
|
|
else:
|
|
if self.p is not None:
|
|
self.p_write(stmt + "\n", True)
|
|
self.smt2cache[-1].append(stmt)
|
|
else:
|
|
self.p_write(stmt + "\n", True)
|
|
|
|
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
|
|
|
|
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]
|
|
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])
|
|
|
|
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")
|
|
|
|
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])
|
|
|
|
def hiernets(self, top, regs_only=False):
|
|
def hiernets_worker(nets, mod, cursor):
|
|
for netname in sorted(self.modinfo[mod].wsize.keys()):
|
|
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
|
|
|
|
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
|
|
|
|
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")
|
|
|
|
count_brackets += line.count("(")
|
|
count_brackets -= line.count(")")
|
|
stmt.append(line)
|
|
|
|
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)
|
|
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()
|
|
sys.exit(1)
|
|
|
|
return stmt
|
|
|
|
def check_sat(self):
|
|
if self.debug_print:
|
|
print("> (check-sat)")
|
|
if self.debug_file and not self.nocomments:
|
|
print("; running check-sat..", file=self.debug_file)
|
|
self.debug_file.flush()
|
|
|
|
if self.solver != "dummy":
|
|
if self.noincr:
|
|
if self.p is not None:
|
|
self.p_close()
|
|
self.p_open()
|
|
for cache_ctx in self.smt2cache:
|
|
for cache_stmt in cache_ctx:
|
|
self.p_write(cache_stmt + "\n", False)
|
|
|
|
self.p_write("(check-sat)\n", True)
|
|
|
|
if self.timeinfo:
|
|
i = 0
|
|
s = "/-\|"
|
|
|
|
count = 0
|
|
num_bs = 0
|
|
while self.p_poll():
|
|
count += 1
|
|
|
|
if count < 25:
|
|
continue
|
|
|
|
if count % 10 == 0 or count == 25:
|
|
secs = count // 10
|
|
|
|
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)
|
|
|
|
print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
|
|
num_bs = len(m) + 3
|
|
|
|
else:
|
|
print("\b" + s[i], end="", file=sys.stderr)
|
|
|
|
sys.stderr.flush()
|
|
i = (i + 1) % len(s)
|
|
|
|
if num_bs != 0:
|
|
print("\b \b" * num_bs, end="", file=sys.stderr)
|
|
sys.stderr.flush()
|
|
|
|
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)
|
|
|
|
result = self.read()
|
|
|
|
if self.debug_file:
|
|
print("(set-info :status %s)" % result, file=self.debug_file)
|
|
print("(check-sat)", file=self.debug_file)
|
|
self.debug_file.flush()
|
|
|
|
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)
|
|
|
|
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]
|
|
|
|
def unparse(self, stmt):
|
|
if isinstance(stmt, list):
|
|
return "(" + " ".join([self.unparse(s) for s in stmt]) + ")"
|
|
return stmt
|
|
|
|
def bv2hex(self, v):
|
|
h = ""
|
|
v = self.bv2bin(v)
|
|
while len(v) > 0:
|
|
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))
|
|
if v == "true": return "1"
|
|
if v == "false": return "0"
|
|
if v.startswith("#b"):
|
|
return v[2:]
|
|
if v.startswith("#x"):
|
|
return "".join(hex_dict.get(x) for x in v[2:])
|
|
assert False
|
|
|
|
def bv2int(self, v):
|
|
return int(self.bv2bin(v), 2)
|
|
|
|
def get(self, expr):
|
|
self.write("(get-value (%s))" % (expr))
|
|
return self.parse(self.read())[0][1]
|
|
|
|
def get_list(self, expr_list):
|
|
if len(expr_list) == 0:
|
|
return []
|
|
self.write("(get-value (%s))" % " ".join(expr_list))
|
|
return [n[1] for n in self.parse(self.read())]
|
|
|
|
def get_path(self, mod, path):
|
|
assert mod in self.modinfo
|
|
path = path.replace("\\", "/").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)
|
|
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):
|
|
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)
|
|
|
|
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)
|
|
|
|
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))
|
|
|
|
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])
|
|
|
|
def get_net_hex(self, mod_name, net_path, state_name):
|
|
return self.bv2hex(self.get_net(mod_name, net_path, state_name))
|
|
|
|
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))
|
|
|
|
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)]
|
|
|
|
def wait(self):
|
|
if self.p is not None:
|
|
self.p.wait()
|
|
self.p_close()
|
|
|
|
|
|
class SmtOpts:
|
|
def __init__(self):
|
|
self.shortopts = "s:S:v"
|
|
self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
|
|
self.solver = "yices"
|
|
self.solver_opts = list()
|
|
self.debug_print = False
|
|
self.debug_file = None
|
|
self.dummy_file = None
|
|
self.unroll = False
|
|
self.noincr = False
|
|
self.timeinfo = os.name != "nt"
|
|
self.logic = None
|
|
self.info_stmts = list()
|
|
self.nocomments = False
|
|
|
|
def handle(self, o, a):
|
|
if o == "-s":
|
|
self.solver = a
|
|
elif o == "-S":
|
|
self.solver_opts.append(a)
|
|
elif o == "-v":
|
|
self.debug_print = True
|
|
elif o == "--unroll":
|
|
self.unroll = True
|
|
elif o == "--noincr":
|
|
self.noincr = True
|
|
elif o == "--noprogress":
|
|
self.timeinfo = False
|
|
elif o == "--dump-smt2":
|
|
self.debug_file = open(a, "w")
|
|
elif o == "--logic":
|
|
self.logic = a
|
|
elif o == "--dummy":
|
|
self.dummy_file = a
|
|
elif o == "--info":
|
|
self.info_stmts.append(a)
|
|
elif o == "--nocomments":
|
|
self.nocomments = True
|
|
else:
|
|
return False
|
|
return True
|
|
|
|
def helpmsg(self):
|
|
return """
|
|
-s <solver>
|
|
set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
|
|
default: yices
|
|
|
|
-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
|
|
|
|
-v
|
|
enable debug output
|
|
|
|
--unroll
|
|
unroll uninterpreted functions
|
|
|
|
--noincr
|
|
don't use incremental solving, instead restart solver for
|
|
each (check-sat). This also avoids (push) and (pop).
|
|
|
|
--noprogress
|
|
disable timer display during solving
|
|
(this option is set implicitly on Windows)
|
|
|
|
--dump-smt2 <filename>
|
|
write smt2 statements to file
|
|
|
|
--info <smt2-info-stmt>
|
|
include the specified smt2 info statement in the smt2 output
|
|
|
|
--nocomments
|
|
strip all comments from the generated smt2 code
|
|
"""
|
|
|
|
|
|
class MkVcd:
|
|
def __init__(self, f):
|
|
self.f = f
|
|
self.t = -1
|
|
self.nets = dict()
|
|
self.clocks = dict()
|
|
|
|
def add_net(self, path, width):
|
|
path = tuple(path)
|
|
assert self.t == -1
|
|
key = "n%d" % len(self.nets)
|
|
self.nets[path] = (key, width)
|
|
|
|
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)
|
|
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)
|
|
|
|
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
|
|
|
|
def set_time(self, t):
|
|
assert t >= self.t
|
|
if t != self.t:
|
|
if self.t == -1:
|
|
print("$version Generated by Yosys-SMTBMC $end", file=self.f)
|
|
print("$timescale 1ns $end", file=self.f)
|
|
print("$var integer 32 t smt_step $end", file=self.f)
|
|
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:
|
|
scopename = uipath[len(scope)]
|
|
if scopename.startswith("$"):
|
|
scopename = "\\" + scopename
|
|
print("$scope module %s $end" % scopename, 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)
|
|
|
|
print("$enddefinitions $end", file=self.f)
|
|
|
|
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)
|
|
print("1!", file=self.f)
|
|
print("b%s t" % format(self.t, "032b"), file=self.f)
|
|
|
|
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)
|