diff options
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 63 |
1 files changed, 58 insertions, 5 deletions
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): |