diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 14 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 63 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 101 |
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 """ |