aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/smt2/smt2.cc8
-rw-r--r--backends/smt2/smtbmc.py52
-rw-r--r--backends/smt2/smtio.py161
3 files changed, 139 insertions, 82 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e07515133..9a25f3a23 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -998,7 +998,7 @@ struct Smt2Backend : public Backend {
continue;
}
if (args[argidx] == "-nomem") {
- bvmode = false;
+ memmode = false;
continue;
}
if (args[argidx] == "-wires") {
@@ -1027,6 +1027,12 @@ struct Smt2Backend : public Backend {
*f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str);
+ if (!bvmode)
+ *f << stringf("; yosys-smt2-nobv\n");
+
+ if (!memmode)
+ *f << stringf("; yosys-smt2-nomem\n");
+
std::vector<RTLIL::Module*> sorted_modules;
// extract module dependencies
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index fa4966089..bb763647c 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -35,6 +35,7 @@ dumpall = False
assume_skipped = None
final_only = False
topmod = None
+noinfo = False
so = SmtOpts()
@@ -60,6 +61,10 @@ yosys-smtbmc [options] <yosys_smt2_output>
--smtc <constr_filename>
read constraints file
+ --noinfo
+ only run the core proof, do not collect and print any
+ additional information (e.g. which assert failed)
+
--final-only
only check final constraints, assume base case
@@ -89,7 +94,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
- ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all"])
+ ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"])
except:
usage()
@@ -121,6 +126,8 @@ for o, a in opts:
outconstr = a
elif o == "--dump-all":
dumpall = True
+ elif o == "--noinfo":
+ noinfo = True
elif o == "-i":
tempind = True
elif o == "-g":
@@ -136,11 +143,6 @@ if len(args) != 1:
usage()
-if tempind and len(inconstr) != 0:
- print("Error: options -i and --smtc are exclusive.")
- sys.exit(1)
-
-
constr_final_start = None
constr_asserts = defaultdict(list)
constr_assumes = defaultdict(list)
@@ -163,7 +165,8 @@ for fn in inconstr:
if tokens[0] == "initial":
current_states = set()
- current_states.add(0)
+ if not tempind:
+ current_states.add(0)
continue
if tokens[0] == "final":
@@ -182,20 +185,21 @@ for fn in inconstr:
if tokens[0] == "state":
current_states = set()
- for token in tokens[1:]:
- tok = token.split(":")
- if len(tok) == 1:
- current_states.add(int(token))
- elif len(tok) == 2:
- lower = int(tok[0])
- if tok[1] == "*":
- upper = num_steps
+ if not tempind:
+ for token in tokens[1:]:
+ tok = token.split(":")
+ if len(tok) == 1:
+ current_states.add(int(token))
+ elif len(tok) == 2:
+ lower = int(tok[0])
+ if tok[1] == "*":
+ upper = num_steps
+ else:
+ upper = int(tok[1])
+ for i in range(lower, upper+1):
+ current_states.add(i)
else:
- upper = int(tok[1])
- for i in range(lower, upper+1):
- current_states.add(i)
- else:
- assert 0
+ assert 0
continue
if tokens[0] == "always":
@@ -281,12 +285,10 @@ def print_msg(msg):
sys.stdout.flush()
print_msg("Solver: %s" % (so.solver))
-smt.setup("QF_AUFBV")
with open(args[0], "r") as f:
for line in f:
smt.write(line)
- smt.info(line)
if topmod is None:
topmod = smt.topmod
@@ -490,6 +492,7 @@ def print_failed_asserts_worker(mod, state, path):
def print_failed_asserts(state, final=False):
+ if noinfo: return
loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
for loc, expr, value in zip(loc_list, expr_list, value_list):
@@ -511,6 +514,7 @@ def print_anyconsts_worker(mod, state, path):
def print_anyconsts(state):
+ if noinfo: return
print_anyconsts_worker(topmod, "s%d" % state, topmod)
@@ -522,13 +526,15 @@ if tempind:
smt.write("(assert (|%s_u| s%d))" % (topmod, step))
smt.write("(assert (|%s_h| s%d))" % (topmod, step))
smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
+ smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
if step == num_steps:
- smt.write("(assert (not (|%s_a| s%d)))" % (topmod, step))
+ smt.write("(assert (not (and (|%s_a| s%d) %s)))" % (topmod, step, get_constr_expr(constr_asserts, step)))
else:
smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step, step+1))
smt.write("(assert (|%s_a| s%d))" % (topmod, step))
+ smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
if step > num_steps-skip_steps:
print_msg("Skipping induction in step %d.." % (step))
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 5d0a78485..58554572d 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -47,11 +47,19 @@ class SmtModInfo:
class SmtIo:
- def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, unroll=None, opts=None):
+ def __init__(self, opts=None):
+ self.logic = None
+ self.logic_qf = True
+ self.logic_ax = True
+ self.logic_uf = True
+ self.logic_bv = True
+
if opts is not None:
+ self.logic = opts.logic
self.solver = opts.solver
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
@@ -59,24 +67,10 @@ class SmtIo:
self.solver = "z3"
self.debug_print = False
self.debug_file = None
+ self.dummy_file = None
self.timeinfo = True
self.unroll = False
- if solver is not None:
- self.solver = solver
-
- if debug_print is not None:
- self.debug_print = debug_print
-
- if debug_file is not None:
- self.debug_file = debug_file
-
- if timeinfo is not None:
- self.timeinfo = timeinfo
-
- if unroll is not None:
- self.unroll = unroll
-
if self.solver == "yices":
popen_vargs = ['yices-smt2', '--incremental']
@@ -93,7 +87,16 @@ class SmtIo:
popen_vargs = ['boolector', '--smt2', '-i']
self.unroll = 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")
+ self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+
if self.unroll:
+ self.logic_uf = False
self.unroll_idcnt = 0
self.unroll_buffer = ""
self.unroll_sorts = set()
@@ -102,20 +105,26 @@ class SmtIo:
self.unroll_cache = dict()
self.unroll_stack = list()
- self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
self.start_time = time()
self.modinfo = dict()
self.curmod = None
self.topmod = None
+ self.setup_done = False
+
+ def setup(self):
+ assert not self.setup_done
+
+ 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"
- def setup(self, logic="ALL", info=None):
+ self.setup_done = True
self.write("(set-option :produce-models true)")
- self.write("(set-logic %s)" % logic)
- if info is not None:
- self.write("(set-info :source |%s|)" % info)
- self.write("(set-info :smt-lib-version 2.5)")
- self.write("(set-info :category \"industrial\")")
+ self.write("(set-logic %s)" % self.logic)
def timestamp(self):
secs = int(time() - self.start_time)
@@ -171,6 +180,11 @@ class SmtIo:
return stmt
def write(self, stmt, unroll=True):
+ if stmt.startswith(";"):
+ self.info(stmt)
+ elif not self.setup_done:
+ self.setup()
+
stmt = stmt.strip()
if unroll and self.unroll:
@@ -231,8 +245,9 @@ class SmtIo:
print(stmt, file=self.debug_file)
self.debug_file.flush()
- self.p.stdin.write(bytes(stmt + "\n", "ascii"))
- self.p.stdin.flush()
+ if self.solver != "dummy":
+ self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+ self.p.stdin.flush()
def info(self, stmt):
if not stmt.startswith("; yosys-smt2-"):
@@ -240,6 +255,14 @@ class SmtIo:
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-module":
self.curmod = fields[2]
self.modinfo[self.curmod] = SmtModInfo()
@@ -303,15 +326,22 @@ class SmtIo:
count_brackets = 0
while True:
- line = self.p.stdout.readline().decode("ascii").strip()
+ if self.solver == "dummy":
+ line = self.dummy_fd.readline().strip()
+ else:
+ line = self.p.stdout.readline().decode("ascii").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.p.poll():
+ if self.solver != "dummy" and self.p.poll():
print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
sys.exit(1)
@@ -329,43 +359,44 @@ class SmtIo:
print("; running check-sat..", file=self.debug_file)
self.debug_file.flush()
- self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
- self.p.stdin.flush()
+ if self.solver != "dummy":
+ self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
+ self.p.stdin.flush()
- if self.timeinfo:
- i = 0
- s = "/-\|"
+ if self.timeinfo:
+ i = 0
+ s = "/-\|"
- count = 0
- num_bs = 0
- while select([self.p.stdout], [], [], 0.1) == ([], [], []):
- count += 1
+ count = 0
+ num_bs = 0
+ while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+ count += 1
- if count < 25:
- continue
+ if count < 25:
+ continue
- if count % 10 == 0 or count == 25:
- secs = count // 10
+ 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)
+ 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
+ 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)
+ else:
+ print("\b" + s[i], end="", file=sys.stderr)
- sys.stderr.flush()
- i = (i + 1) % len(s)
+ sys.stderr.flush()
+ i = (i + 1) % len(s)
- if num_bs != 0:
- print("\b \b" * num_bs, end="", file=sys.stderr)
- sys.stderr.flush()
+ if num_bs != 0:
+ print("\b \b" * num_bs, end="", file=sys.stderr)
+ sys.stderr.flush()
result = self.read()
if self.debug_file:
@@ -524,18 +555,21 @@ class SmtIo:
return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
def wait(self):
- self.p.wait()
+ if self.solver != "dummy":
+ self.p.wait()
class SmtOpts:
def __init__(self):
self.shortopts = "s:v"
- self.longopts = ["unroll", "no-progress", "dump-smt2="]
+ self.longopts = ["unroll", "no-progress", "dump-smt2=", "logic=", "dummy="]
self.solver = "z3"
self.debug_print = False
self.debug_file = None
+ self.dummy_file = None
self.unroll = False
self.timeinfo = True
+ self.logic = None
def handle(self, o, a):
if o == "-s":
@@ -548,6 +582,10 @@ class SmtOpts:
self.timeinfo = True
elif o == "--dump-smt2":
self.debug_file = open(a, "w")
+ elif o == "--logic":
+ self.logic = a
+ elif o == "--dummy":
+ self.dummy_file = a
else:
return False
return True
@@ -555,9 +593,16 @@ class SmtOpts:
def helpmsg(self):
return """
-s <solver>
- set SMT solver: z3, cvc4, yices, mathsat
+ set SMT solver: z3, cvc4, yices, mathsat, boolector, dummy
default: z3
+ --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
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-08 19:40:42 +0000