summaryrefslogtreecommitdiff
path: root/backends/smt2
diff options
context:
space:
mode:
authorRuben Undheim <ruben.undheim@gmail.com>2016-11-03 23:18:00 +0100
committerRuben Undheim <ruben.undheim@gmail.com>2016-11-03 23:18:00 +0100
commitfefe0fc0430f4f173a25e674708aa0f4f0854b31 (patch)
treeadb13b830212c269d58031f900d652f29013d2d7 /backends/smt2
parent4f096fe65b77435daba019248273e547fa18d167 (diff)
Imported yosys 0.7
Diffstat (limited to 'backends/smt2')
-rw-r--r--backends/smt2/smt2.cc14
-rw-r--r--backends/smt2/smtbmc.py63
-rw-r--r--backends/smt2/smtio.py101
3 files changed, 150 insertions, 28 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9a25f3a2..ddac6900 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -379,7 +379,7 @@ struct Smt2Worker
return;
}
- if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+ if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
@@ -407,7 +407,7 @@ struct Smt2Worker
if (bvmode)
{
- if (cell->type == "$dff")
+ if (cell->type.in("$ff", "$dff"))
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
@@ -417,7 +417,7 @@ struct Smt2Worker
return;
}
- if (cell->type == "$anyconst")
+ if (cell->type.in("$anyconst", "$anyseq"))
{
registers.insert(cell);
decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
@@ -586,7 +586,7 @@ struct Smt2Worker
return;
}
- log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv or -mem mode?)\n",
+ log_error("Unsupported cell type %s for cell %s.%s.\n",
log_id(cell->type), log_id(module), log_id(cell));
}
@@ -596,7 +596,7 @@ struct Smt2Worker
pool<SigBit> reg_bits;
for (auto cell : module->cells())
- if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) {
+ if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) {
// not using sigmap -- we want the net directly at the dff output
for (auto bit : cell->getPort("\\Q"))
reg_bits.insert(bit);
@@ -674,14 +674,14 @@ struct Smt2Worker
for (auto cell : this_regs)
{
- if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+ if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
{
std::string expr_d = get_bool(cell->getPort("\\D"));
std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
}
- if (cell->type == "$dff")
+ if (cell->type.in("$ff", "$dff"))
{
std::string expr_d = get_bv(cell->getPort("\\D"));
std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index bb763647..04c25f91 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -26,6 +26,7 @@ skip_steps = 0
step_size = 1
num_steps = 20
vcdfile = None
+cexfile = None
vlogtbfile = None
inconstr = list()
outconstr = None
@@ -61,6 +62,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
--smtc <constr_filename>
read constraints file
+ --cex <cex_filename>
+ read cex file as written by ABC's "write_cex -n"
+
--noinfo
only run the core proof, do not collect and print any
additional information (e.g. which assert failed)
@@ -94,7 +98,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", "noinfo"])
+ ["final-only", "assume-skipped=", "smtc=", "cex=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"])
except:
usage()
@@ -118,6 +122,8 @@ for o, a in opts:
final_only = True
elif o == "--smtc":
inconstr.append(a)
+ elif o == "--cex":
+ cexfile = a
elif o == "--dump-vcd":
vcdfile = a
elif o == "--dump-vlogtb":
@@ -146,6 +152,7 @@ if len(args) != 1:
constr_final_start = None
constr_asserts = defaultdict(list)
constr_assumes = defaultdict(list)
+constr_write = list()
for fn in inconstr:
current_states = None
@@ -229,6 +236,14 @@ for fn in inconstr:
continue
+ if tokens[0] == "write":
+ constr_write.append(" ".join(tokens[1:]))
+ continue
+
+ if tokens[0] == "logic":
+ so.logic = " ".join(tokens[1:])
+ continue
+
assert 0
@@ -240,7 +255,7 @@ def get_constr_expr(db, state, final=False, getvalues=False):
if state not in db:
return ([], [], []) if getvalues else "true"
- netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)')
+ netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*)\](?=[ )]|$)')
def replace_netref(match):
state_sel = match.group(2)
@@ -280,6 +295,9 @@ def get_constr_expr(db, state, final=False, getvalues=False):
smt = SmtIo(opts=so)
+if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None:
+ smt.produce_models = False
+
def print_msg(msg):
print("%s %s" % (smt.timestamp(), msg))
sys.stdout.flush()
@@ -290,12 +308,46 @@ with open(args[0], "r") as f:
for line in f:
smt.write(line)
+for line in constr_write:
+ smt.write(line)
+
if topmod is None:
topmod = smt.topmod
assert topmod is not None
assert topmod in smt.modinfo
+if cexfile is not None:
+ with open(cexfile, "r") as f:
+ cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
+ for entry in f.read().split():
+ match = cex_regex.match(entry)
+ assert match
+
+ name, bit, extra_name, step, val = match.group(1), match.group(2), match.group(3), match.group(4), match.group(5)
+
+ if extra_name != "":
+ continue
+
+ if name not in smt.modinfo[topmod].inputs:
+ continue
+
+ if bit is None:
+ bit = 0
+ else:
+ bit = int(bit[1:-1])
+
+ step = int(step[1:])
+ val = int(val)
+
+ if smt.modinfo[topmod].wsize[name] == 1:
+ assert bit == 0
+ smtexpr = "(= [%s] %s)" % (name, "true" if val else "false")
+ else:
+ smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bit, bit, name, val)
+
+ # print("cex@%d: %s" % (step, smtexpr))
+ constr_assumes[step].append((cexfile, smtexpr))
def write_vcd_trace(steps_start, steps_stop, index):
filename = vcdfile.replace("%", index)
@@ -625,9 +677,10 @@ else: # not tempind
smt.write("(pop 1)")
- for i in range(step, last_check_step+1):
- smt.write("(assert (|%s_a| s%d))" % (topmod, i))
- smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
+ if (constr_final_start is not None) or (last_check_step+1 != num_steps):
+ for i in range(step, last_check_step+1):
+ smt.write("(assert (|%s_a| s%d))" % (topmod, i))
+ smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
if constr_final_start is not None:
for i in range(step, last_check_step+1):
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 58554572..865eed1f 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -53,6 +53,9 @@ class SmtIo:
self.logic_ax = True
self.logic_uf = True
self.logic_bv = True
+ self.produce_models = True
+ self.smt2cache = [list()]
+ self.p = None
if opts is not None:
self.logic = opts.logic
@@ -62,6 +65,9 @@ class SmtIo:
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 = "z3"
@@ -70,30 +76,40 @@ class SmtIo:
self.dummy_file = None
self.timeinfo = True
self.unroll = False
+ self.noincr = False
+ self.info_stmts = list()
+ self.nocomments = False
if self.solver == "yices":
- popen_vargs = ['yices-smt2', '--incremental']
+ self.popen_vargs = ['yices-smt2', '--incremental']
if self.solver == "z3":
- popen_vargs = ['z3', '-smt2', '-in']
+ self.popen_vargs = ['z3', '-smt2', '-in']
if self.solver == "cvc4":
- popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
+ self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
if self.solver == "mathsat":
- popen_vargs = ['mathsat']
+ self.popen_vargs = ['mathsat']
if self.solver == "boolector":
- popen_vargs = ['boolector', '--smt2', '-i']
+ self.popen_vargs = ['boolector', '--smt2', '-i']
self.unroll = True
+ if self.solver == "abc":
+ 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")
- self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ if not self.noincr:
+ self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
if self.unroll:
self.logic_uf = False
@@ -123,9 +139,15 @@ class SmtIo:
if self.logic_bv: self.logic += "BV"
self.setup_done = True
- self.write("(set-option :produce-models true)")
+
+ if self.produce_models:
+ self.write("(set-option :produce-models true)")
+
self.write("(set-logic %s)" % self.logic)
+ for stmt in self.info_stmts:
+ self.write(stmt)
+
def timestamp(self):
secs = int(time() - self.start_time)
return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
@@ -187,11 +209,12 @@ class SmtIo:
stmt = stmt.strip()
- if unroll and self.unroll:
+ if self.nocomments or self.unroll:
if stmt.startswith(";"):
return
-
stmt = re.sub(r" ;.*", "", stmt)
+
+ if unroll and self.unroll:
stmt = self.unroll_buffer + stmt
self.unroll_buffer = ""
@@ -246,8 +269,22 @@ class SmtIo:
self.debug_file.flush()
if self.solver != "dummy":
- self.p.stdin.write(bytes(stmt + "\n", "ascii"))
- self.p.stdin.flush()
+ if self.noincr:
+ if self.p is not None and not stmt.startswith("(get-"):
+ self.p.stdin.close()
+ self.p = None
+ if stmt == "(push 1)":
+ self.smt2cache.append(list())
+ elif stmt == "(pop 1)":
+ self.smt2cache.pop()
+ else:
+ if self.p is not None:
+ self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+ self.p.stdin.flush()
+ self.smt2cache[-1].append(stmt)
+ else:
+ self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+ self.p.stdin.flush()
def info(self, stmt):
if not stmt.startswith("; yosys-smt2-"):
@@ -355,11 +392,20 @@ class SmtIo:
def check_sat(self):
if self.debug_print:
print("> (check-sat)")
- if self.debug_file:
+ 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.stdin.close()
+ self.p = None
+ self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ for cache_ctx in self.smt2cache:
+ for cache_stmt in cache_ctx:
+ self.p.stdin.write(bytes(cache_stmt + "\n", "ascii"))
+
self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
self.p.stdin.flush()
@@ -495,6 +541,10 @@ class SmtIo:
def net_expr(self, mod, base, path):
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:
@@ -555,21 +605,24 @@ class SmtIo:
return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
def wait(self):
- if self.solver != "dummy":
+ if self.p is not None:
self.p.wait()
class SmtOpts:
def __init__(self):
self.shortopts = "s:v"
- self.longopts = ["unroll", "no-progress", "dump-smt2=", "logic=", "dummy="]
+ self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.solver = "z3"
self.debug_print = False
self.debug_file = None
self.dummy_file = None
self.unroll = False
+ self.noincr = False
self.timeinfo = True
self.logic = None
+ self.info_stmts = list()
+ self.nocomments = False
def handle(self, o, a):
if o == "-s":
@@ -578,7 +631,9 @@ class SmtOpts:
self.debug_print = True
elif o == "--unroll":
self.unroll = True
- elif o == "--no-progress":
+ elif o == "--noincr":
+ self.noincr = True
+ elif o == "--noprogress":
self.timeinfo = True
elif o == "--dump-smt2":
self.debug_file = open(a, "w")
@@ -586,6 +641,10 @@ class SmtOpts:
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
@@ -609,11 +668,21 @@ class SmtOpts:
--unroll
unroll uninterpreted functions
- --no-progress
+ --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
--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
"""