From e54c355b417eb7fa19421176792d01cb7a62d4cb Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 28 Jan 2017 15:14:56 +0100 Subject: [PATCH] Add "yosys-smtbmc --aig-noheader" and AIGER mem init support --- backends/smt2/smtbmc.py | 39 +++++++++++++++++++++++++++++++++------ backends/smt2/smtio.py | 24 ++++++++++++++++++++++-- 2 files changed, 55 insertions(+), 8 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index ecee6795e..ab952786e 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -30,6 +30,7 @@ append_steps = 0 vcdfile = None cexfile = None aigprefix = None +aigheader = True vlogtbfile = None inconstr = list() outconstr = None @@ -73,6 +74,10 @@ yosys-smtbmc [options] and AIGER witness file. The file names are .aim for the map file and .aiw for the witness file. + --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 +116,7 @@ yosys-smtbmc [options] 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() @@ -141,6 +146,8 @@ for o, a in opts: cexfile = a elif o == "--aig": aigprefix = a + elif o == "--aig-noheader": + aigheader = False elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -411,6 +418,9 @@ if aigprefix is not None: 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 +468,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 +596,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 +657,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() diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 497b72db8..3946c3423 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -567,6 +567,26 @@ class SmtIo: assert net_path[-1] in self.modinfo[mod].wsize return self.modinfo[mod].wsize[net_path[-1]] + def net_exists(self, mod, net_path): + for i in range(len(net_path)-1): + if mod not in self.modinfo: return False + if net_path[i] not in self.modinfo[mod].cells: return False + mod = self.modinfo[mod].cells[net_path[i]] + + if mod not in self.modinfo: return False + if net_path[-1] not in self.modinfo[mod].wsize: return False + return True + + def mem_exists(self, mod, mem_path): + for i in range(len(mem_path)-1): + if mod not in self.modinfo: return False + if mem_path[i] not in self.modinfo[mod].cells: return False + mod = self.modinfo[mod].cells[mem_path[i]] + + if mod not in self.modinfo: return False + if mem_path[-1] not in self.modinfo[mod].memories: return False + return True + def mem_expr(self, mod, base, path, portidx=None, infomode=False): if len(path) == 1: assert mod in self.modinfo @@ -582,8 +602,8 @@ class SmtIo: nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode) - def mem_info(self, mod, base, path): - return self.mem_expr(mod, base, path, infomode=True) + def mem_info(self, mod, path): + return self.mem_expr(mod, "", path, infomode=True) def get_net(self, mod_name, net_path, state_name): return self.get(self.net_expr(mod_name, state_name, net_path))