From: Clifford Wolf Date: Sun, 21 Aug 2016 13:56:22 +0000 (+0200) Subject: yosys-smtbmc: improved --dump-vlogtb handling of memories X-Git-Tag: yosys-0.7~114 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7a33b9892a7a542ca1ac0b503c4368a1721a9afb;p=yosys.git yosys-smtbmc: improved --dump-vlogtb handling of memories --- diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 9acbfbeb8..aaafc3f9a 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -460,19 +460,23 @@ struct Smt2Worker decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", log_id(module), arrayid, log_id(module), abits, width, log_id(cell))); - decls.push_back(stringf("; yosys-smt2-memory %s %d %d\n", log_id(cell), abits, width)); + decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d\n", log_id(cell), abits, width, rd_ports)); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n", log_id(module), log_id(cell), log_id(module), abits, width, log_id(module), arrayid)); for (int i = 0; i < rd_ports; i++) { - std::string addr = get_bv(cell->getPort("\\RD_ADDR").extract(abits*i, abits)); + SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits); SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width); + std::string addr = get_bv(addr_sig); if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool()) log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! " "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module)); + decls.push_back(stringf("(define-fun |%s_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + log_id(module), i, log_id(cell), log_id(module), abits, addr.c_str(), log_signal(addr_sig))); + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) %s)) ; %s\n", log_id(module), idcounter, log_id(module), width, log_id(module), arrayid, addr.c_str(), log_signal(data_sig))); register_bv(data_sig, idcounter++); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index a6e8bf67a..170671483 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -200,13 +200,23 @@ def write_vlogtb_trace(steps): mems = sorted(smt.hiermems(topmod)) for mempath in mems: - mem, abits, width = smt.mem_expr(topmod, "s0", mempath) + abits, width, ports = smt.mem_info(topmod, "s0", mempath) + mem = smt.mem_expr(topmod, "s0", mempath) + + addr_expr_list = list() + for i in range(steps): + for j in range(ports): + addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j)) + + addr_list = set() + for val in smt.get_list(addr_expr_list): + addr_list.add(smt.bv2int(val)) expr_list = list() - for i in range(2**abits): + for i in addr_list: expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits))) - for i, val in enumerate(smt.get_list(expr_list)): + for i, val in zip(addr_list, smt.get_list(expr_list)): val = smt.bv2bin(val) print(" UUT.%s[%d] = %d'b%s;" % (".".join(mempath), i, len(val), val), file=f) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 24c28182a..8480891b0 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -128,7 +128,7 @@ class smtio: self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3]) if fields[1] == "yosys-smt2-memory": - self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4])) + self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5])) if fields[1] == "yosys-smt2-wire": self.modinfo[self.curmod].wires.add(fields[2]) @@ -309,6 +309,9 @@ class smtio: return "".join(digits) assert False + def bv2int(self, v): + return int(self.bv2bin(v), 2) + def get(self, expr): self.write("(get-value (%s))" % (expr)) return self.parse(self.read())[0][1] @@ -342,11 +345,13 @@ class smtio: assert net_path[-1] in self.modinfo[mod].wsize return self.modinfo[mod].wsize[net_path[-1]] - def mem_expr(self, mod, base, path): + def mem_expr(self, mod, base, path, portidx=None, infomode=False): if len(path) == 1: assert mod in self.modinfo assert path[0] in self.modinfo[mod].memories - return "(|%s_m %s| %s)" % (mod, path[0], base), self.modinfo[mod].memories[path[0]][0], self.modinfo[mod].memories[path[0]][1] + if infomode: + return self.modinfo[mod].memories[path[0]] + return "(|%s_m%s %s| %s)" % (mod, "" if portidx is None else ":%d" % portidx, path[0], base) assert mod in self.modinfo assert path[0] in self.modinfo[mod].cells @@ -355,6 +360,9 @@ class smtio: nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) return self.mem_expr(nextmod, nextbase, path[1:]) + def mem_info(self, mod, base, path): + return self.mem_expr(mod, base, 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))