diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smtbmc.py | 133 |
1 files changed, 127 insertions, 6 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 3384789ee..56c7bccc1 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -22,12 +22,14 @@ import os, sys, getopt, re from smtio import SmtIo, SmtOpts, MkVcd from collections import defaultdict +got_topt = False skip_steps = 0 step_size = 1 num_steps = 20 append_steps = 0 vcdfile = None cexfile = None +aigprefix = None vlogtbfile = None inconstr = list() outconstr = None @@ -66,6 +68,11 @@ yosys-smtbmc [options] <yosys_smt2_output> --cex <cex_filename> read cex file as written by ABC's "write_cex -n" + --aig <prefix> + read AIGER map file (as written by Yosys' "write_aiger -map") + and AIGER witness file. The file names are <prefix>.aim for + the map file and <prefix>.aiw for the witness file. + --noinfo only run the core proof, do not collect and print any additional information (e.g. which assert failed) @@ -104,12 +111,14 @@ 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=", "cex=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="]) + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", + "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="]) except: usage() for o, a in opts: if o == "-t": + got_topt = True a = a.split(":") if len(a) == 1: num_steps = int(a[0]) @@ -121,7 +130,7 @@ for o, a in opts: step_size = int(a[1]) num_steps = int(a[2]) else: - assert 0 + assert False elif o == "--assume-skipped": assume_skipped = int(a) elif o == "--final-only": @@ -130,6 +139,8 @@ for o, a in opts: inconstr.append(a) elif o == "--cex": cexfile = a + elif o == "--aig": + aigprefix = a elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -195,7 +206,7 @@ for fn in inconstr: current_states = set(["final-%d" % i for i in range(-i, num_steps+1)]) constr_final_start = -i if constr_final_start is None else min(constr_final_start, -i) else: - assert 0 + assert False continue if tokens[0] == "state": @@ -214,7 +225,7 @@ for fn in inconstr: for i in range(lower, upper+1): current_states.add(i) else: - assert 0 + assert False continue if tokens[0] == "always": @@ -225,7 +236,7 @@ for fn in inconstr: assert i < 0 current_states = set(range(-i, num_steps+1)) else: - assert 0 + assert False continue if tokens[0] == "assert": @@ -252,7 +263,7 @@ for fn in inconstr: so.logic = " ".join(tokens[1:]) continue - assert 0 + assert False def get_constr_expr(db, state, final=False, getvalues=False): @@ -357,6 +368,116 @@ if cexfile is not None: # print("cex@%d: %s" % (step, smtexpr)) constr_assumes[step].append((cexfile, smtexpr)) +if aigprefix is not None: + input_map = dict() + init_map = dict() + latch_map = dict() + + with open(aigprefix + ".aim", "r") as f: + for entry in f.read().splitlines(): + entry = entry.split() + + if entry[0] == "input": + input_map[int(entry[1])] = (entry[3], int(entry[2])) + continue + + if entry[0] == "init": + init_map[int(entry[1])] = (entry[3], int(entry[2])) + continue + + if entry[0] in ["latch", "invlatch"]: + latch_map[int(entry[1])] = (entry[3], int(entry[2]), entry[0] == "invlatch") + continue + + if entry[0] in ["output", "wire"]: + continue + + assert False + + with open(aigprefix + ".aiw", "r") as f: + got_state = False + got_ffinit = False + step = 0 + + for entry in f.read().splitlines(): + if len(entry) == 0 or entry[0] in "bcjfu.": + continue + + if not got_state: + got_state = True + assert entry == "1" + continue + + if not got_ffinit: + got_ffinit = True + if len(init_map) == 0: + for i in range(len(entry)): + if entry[i] == "x": + continue + + if i in latch_map: + value = int(entry[i]) + name = latch_map[i][0] + bitidx = latch_map[i][1] + invert = latch_map[i][2] + + if invert: + value = 1 - value + + path = smt.get_path(topmod, name) + width = smt.net_width(topmod, path) + + if width == 1: + assert bitidx == 0 + smtexpr = "(= [%s] %s)" % (name, "true" if value else "false") + else: + smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value) + + constr_assumes[0].append((cexfile, smtexpr)) + continue + + for i in range(len(entry)): + if entry[i] == "x": + continue + + if (step == 0) and (i in init_map): + value = int(entry[i]) + name = init_map[i][0] + bitidx = init_map[i][1] + + path = smt.get_path(topmod, name) + width = smt.net_width(topmod, path) + + if width == 1: + assert bitidx == 0 + smtexpr = "(= [%s] %s)" % (name, "true" if value else "false") + else: + smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value) + + constr_assumes[0].append((cexfile, smtexpr)) + + if i in input_map: + value = int(entry[i]) + name = input_map[i][0] + bitidx = input_map[i][1] + + path = smt.get_path(topmod, name) + width = smt.net_width(topmod, path) + + if width == 1: + assert bitidx == 0 + smtexpr = "(= [%s] %s)" % (name, "true" if value else "false") + else: + smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value) + + constr_assumes[step].append((cexfile, smtexpr)) + + if not got_topt: + skip_steps = step + assume_skipped = 0 + num_steps = max(num_steps, step+1) + step += 1 + def write_vcd_trace(steps_start, steps_stop, index): filename = vcdfile.replace("%", index) print_msg("Writing trace to VCD file: %s" % (filename)) |