#
# yosys -- Yosys Open SYnthesis Suite
#
-# Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+# Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
#
# Permission to use, copy, modify, and/or distribute this software for any
# purpose with or without fee is hereby granted, provided that the above
import subprocess
if os.name == "posix":
import resource
-from copy import deepcopy
+from copy import copy
from select import select
from time import time
from queue import Queue, Empty
smtio_stacksize = 128 * 1024 * 1024
if os.uname().sysname == "Darwin":
# MacOS has rather conservative stack limits
- smtio_stacksize = 16 * 1024 * 1024
+ smtio_stacksize = 8 * 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:
self.cells = dict()
self.asserts = dict()
self.covers = dict()
+ self.maximize = set()
+ self.minimize = set()
self.anyconsts = dict()
self.anyseqs = dict()
self.allconsts = dict()
self.logic_bv = True
self.logic_dt = False
self.forall = False
+ self.timeout = 0
self.produce_models = True
self.smt2cache = [list()]
+ self.smt2_options = dict()
self.p = None
self.p_index = solvers_index
solvers_index += 1
self.debug_file = opts.debug_file
self.dummy_file = opts.dummy_file
self.timeinfo = opts.timeinfo
+ self.timeout = opts.timeout
self.unroll = opts.unroll
self.noincr = opts.noincr
self.info_stmts = opts.info_stmts
self.debug_file = None
self.dummy_file = None
self.timeinfo = os.name != "nt"
+ self.timeout = 0
self.unroll = False
self.noincr = False
self.info_stmts = list()
self.unroll = False
if self.solver == "yices":
- if self.noincr:
+ if self.noincr or self.forall:
self.popen_vargs = ['yices-smt2'] + self.solver_opts
else:
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
+ if self.timeout != 0:
+ self.popen_vargs.append('-t')
+ self.popen_vargs.append('%d' % self.timeout);
if self.solver == "z3":
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
+ if self.timeout != 0:
+ self.popen_vargs.append('-T:%d' % self.timeout);
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.timeout != 0:
+ self.popen_vargs.append('--tlimit=%d000' % self.timeout);
if self.solver == "mathsat":
self.popen_vargs = ['mathsat'] + self.solver_opts
+ if self.timeout != 0:
+ print('timeout option is not supported for mathsat.')
+ sys.exit(1)
- if self.solver == "boolector":
+ if self.solver in ["boolector", "bitwuzla"]:
if self.noincr:
- self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts
+ self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts
else:
- self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
+ self.popen_vargs = [self.solver, '--smt2', '-i'] + self.solver_opts
self.unroll = True
+ if self.timeout != 0:
+ print('timeout option is not supported for %s.' % self.solver)
+ sys.exit(1)
if self.solver == "abc":
if len(self.solver_opts) > 0:
self.logic_ax = False
self.unroll = True
self.noincr = True
+ if self.timeout != 0:
+ print('timeout option is not supported for abc.')
+ sys.exit(1)
if self.solver == "dummy":
assert self.dummy_file is not None
if self.logic_uf: self.logic += "UF"
if self.logic_bv: self.logic += "BV"
if self.logic_dt: self.logic = "ALL"
+ if self.solver == "yices" and self.forall: self.logic = "BV"
self.setup_done = True
if self.produce_models:
self.write("(set-option :produce-models true)")
+ #See the SMT-LIB Standard, Section 4.1.7
+ modestart_options = [":global-declarations", ":interactive-mode", ":produce-assertions", ":produce-assignments", ":produce-models", ":produce-proofs", ":produce-unsat-assumptions", ":produce-unsat-cores", ":random-seed"]
+ for key, val in self.smt2_options.items():
+ if key in modestart_options:
+ self.write("(set-option {} {})".format(key, val))
+
self.write("(set-logic %s)" % self.logic)
+ if self.forall and self.solver == "yices":
+ self.write("(set-option :yices-ef-max-iters 1000000000)")
+
+ for key, val in self.smt2_options.items():
+ if key not in modestart_options:
+ self.write("(set-option {} {})".format(key, val))
+
def timestamp(self):
secs = int(time() - self.start_time)
return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)
key = tuple(stmt)
if key not in self.unroll_cache:
- decl = deepcopy(self.unroll_decls[key[0]])
+ decl = copy(self.unroll_decls[key[0]])
self.unroll_cache[key] = "|UNROLL#%d|" % self.unroll_idcnt
decl[1] = self.unroll_cache[key]
if stmt == "(push 1)":
self.unroll_stack.append((
- deepcopy(self.unroll_sorts),
- deepcopy(self.unroll_objs),
- deepcopy(self.unroll_decls),
- deepcopy(self.unroll_cache),
+ copy(self.unroll_sorts),
+ copy(self.unroll_objs),
+ copy(self.unroll_decls),
+ copy(self.unroll_cache),
))
if stmt == "(pop 1)":
fields = stmt.split()
+ if fields[1] == "yosys-smt2-solver-option":
+ self.smt2_options[fields[2]] = fields[3]
+
if fields[1] == "yosys-smt2-nomem":
if self.logic is None:
self.logic_ax = False
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 len(fields) > 4:
+ self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})'
+ else:
+ 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 len(fields) > 4:
+ self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})'
+ else:
+ self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
+
+ if fields[1] == "yosys-smt2-maximize":
+ self.modinfo[self.curmod].maximize.add(fields[2])
+
+ if fields[1] == "yosys-smt2-minimize":
+ self.modinfo[self.curmod].minimize.add(fields[2])
if fields[1] == "yosys-smt2-anyconst":
self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
return stmt
- def check_sat(self):
+ def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted"]):
if self.debug_print:
print("> (check-sat)")
if self.debug_file and not self.nocomments:
if msg is not None:
print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)
- result = self.read()
+ if self.forall:
+ result = self.read()
+ while result not in ["sat", "unsat", "unknown", "timeout", "interrupted", ""]:
+ print("%s %s: %s" % (self.timestamp(), self.solver, result))
+ result = self.read()
+ else:
+ 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 not in expected:
if result == "":
print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
else:
class SmtOpts:
def __init__(self):
self.shortopts = "s:S:v"
- self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
+ self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.solver = "yices"
self.solver_opts = list()
self.debug_print = False
self.unroll = False
self.noincr = False
self.timeinfo = os.name != "nt"
+ self.timeout = 0
self.logic = None
self.info_stmts = list()
self.nocomments = False
self.solver = a
elif o == "-S":
self.solver_opts.append(a)
+ elif o == "--timeout":
+ self.timeout = int(a)
elif o == "-v":
self.debug_print = True
elif o == "--unroll":
def helpmsg(self):
return """
-s <solver>
- set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
+ set SMT solver: z3, yices, boolector, bitwuzla, cvc4, mathsat, dummy
default: yices
-S <opt>
pass <opt> as command line argument to the solver
+ --timeout <value>
+ set the solver timeout to the specified value (in seconds).
+
--logic <smt2_logic>
use the specified SMT2 logic (e.g. QF_AUFBV)
projects / yosys.git / blobdiff