diff options
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 58 |
1 files changed, 47 insertions, 11 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index ecee6795e..10875f523 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -29,7 +29,9 @@ num_steps = 20 append_steps = 0 vcdfile = None cexfile = None -aigprefix = None +aimfile = None +aiwfile = None +aigheader = True vlogtbfile = None inconstr = list() outconstr = None @@ -73,6 +75,14 @@ yosys-smtbmc [options] <yosys_smt2_output> and AIGER witness file. The file names are <prefix>.aim for the map file and <prefix>.aiw for the witness file. + --aig <aim_filename>:<aiw_filename> + like above, but for map files and witness files that do not + share a filename prefix (or use differen file extensions). + + --aig-noheader + the AIGER witness file does not include the status and + properties lines. + --noinfo only run the core proof, do not collect and print any additional information (e.g. which assert failed) @@ -111,7 +121,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=", "cex=", "aig=", + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="]) except: usage() @@ -140,7 +150,13 @@ for o, a in opts: elif o == "--cex": cexfile = a elif o == "--aig": - aigprefix = a + if ":" in a: + aimfile, aiwfile = a.split(":") + else: + aimfile = a + ".aim" + aiwfile = a + ".aiw" + elif o == "--aig-noheader": + aigheader = False elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -375,7 +391,7 @@ if cexfile is not None: skip_steps = max(skip_steps, step) num_steps = max(num_steps, step+1) -if aigprefix is not None: +if aimfile is not None: input_map = dict() init_map = dict() latch_map = dict() @@ -385,7 +401,7 @@ if aigprefix is not None: skip_steps = 0 num_steps = 0 - with open(aigprefix + ".aim", "r") as f: + with open(aimfile, "r") as f: for entry in f.read().splitlines(): entry = entry.split() @@ -406,11 +422,14 @@ if aigprefix is not None: assert False - with open(aigprefix + ".aiw", "r") as f: + with open(aiwfile, "r") as f: got_state = False got_ffinit = False step = 0 + if not aigheader: + got_state = True + for entry in f.read().splitlines(): if len(entry) == 0 or entry[0] in "bcjfu.": continue @@ -458,13 +477,30 @@ if aigprefix is not None: bitidx = init_map[i][1] path = smt.get_path(topmod, name) - width = smt.net_width(topmod, path) + + if not smt.net_exists(topmod, path): + match = re.match(r"(.*)\[(\d+)\]$", path[-1]) + if match: + path[-1] = match.group(1) + addr = int(match.group(2)) + + if not match or not smt.mem_exists(topmod, path): + print_msg("Ignoring init value for unknown net: %s" % (name)) + continue + + meminfo = smt.mem_info(topmod, path) + smtexpr = "(select [%s] #b%s)" % (".".join(path), bin(addr)[2:].zfill(meminfo[0])) + width = meminfo[1] + + else: + smtexpr = "[%s]" % name + width = smt.net_width(topmod, path) if width == 1: assert bitidx == 0 - smtexpr = "(= [%s] %s)" % (name, "true" if value else "false") + smtexpr = "(= %s %s)" % (smtexpr, "true" if value else "false") else: - smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value) + smtexpr = "(= ((_ extract %d %d) %s) #b%d)" % (bitidx, bitidx, smtexpr, value) constr_assumes[0].append((cexfile, smtexpr)) @@ -569,7 +605,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index): mems = sorted(smt.hiermems(topmod)) for mempath in mems: - abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath) + abits, width, ports = smt.mem_info(topmod, mempath) mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath) addr_expr_list = list() @@ -630,7 +666,7 @@ def write_constr_trace(steps_start, steps_stop, index): mems = sorted(smt.hiermems(topmod)) for mempath in mems: - abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath) + abits, width, ports = smt.mem_info(topmod, mempath) mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath) addr_expr_list = list() |