From ed785194def450e68f217a3ae1764b5c5a679298 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 20 Aug 2016 18:42:32 +0200 Subject: [PATCH] Added support for memories to smtio.py --- backends/smt2/smtio.py | 39 +++++++++++++++++++++++++++++++++++---- 1 file changed, 35 insertions(+), 4 deletions(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 8a8033c06..24c28182a 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -27,6 +27,7 @@ class smtmodinfo: self.inputs = set() self.outputs = set() self.registers = set() + self.memories = dict() self.wires = set() self.wsize = dict() self.cells = dict() @@ -126,6 +127,9 @@ class smtio: self.modinfo[self.curmod].registers.add(fields[2]) 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])) + if fields[1] == "yosys-smt2-wire": self.modinfo[self.curmod].wires.add(fields[2]) self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3]) @@ -133,10 +137,11 @@ class smtio: if fields[1] == "yosys-smt2-assert": self.modinfo[self.curmod].asserts[fields[2]] = fields[3] - def hiernets(self, top): + def hiernets(self, top, regs_only=False): def hiernets_worker(nets, mod, cursor): for netname in sorted(self.modinfo[mod].wsize.keys()): - nets.append(cursor + [netname]) + if not regs_only or netname in self.modinfo[mod].registers: + nets.append(cursor + [netname]) for cellname, celltype in sorted(self.modinfo[mod].cells.items()): hiernets_worker(nets, celltype, cursor + [cellname]) @@ -144,6 +149,17 @@ class smtio: hiernets_worker(nets, top, []) return nets + def hiermems(self, top): + def hiermems_worker(mems, mod, cursor): + for memname in sorted(self.modinfo[mod].memories.keys()): + mems.append(cursor + [memname]) + for cellname, celltype in sorted(self.modinfo[mod].cells.items()): + hiermems_worker(mems, celltype, cursor + [cellname]) + + mems = list() + hiermems_worker(mems, top, []) + return mems + def read(self): stmt = [] count_brackets = 0 @@ -298,8 +314,10 @@ class smtio: return self.parse(self.read())[0][1] def get_list(self, expr_list): - self.write("(get-value (%s))" % " ".join(expr_list)) - return [n[1] for n in self.parse(self.read())] + if len(expr_list) == 0: + return [] + self.write("(get-value (%s))" % " ".join(expr_list)) + return [n[1] for n in self.parse(self.read())] def net_expr(self, mod, base, path): if len(path) == 1: @@ -324,6 +342,19 @@ 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): + 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] + + assert mod in self.modinfo + assert path[0] in self.modinfo[mod].cells + + nextmod = self.modinfo[mod].cells[path[0]] + nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) + return self.mem_expr(nextmod, nextbase, path[1:]) + def get_net(self, mod_name, net_path, state_name): return self.get(self.net_expr(mod_name, state_name, net_path)) -- 2.30.2