diff options
Diffstat (limited to 'backends/smt2/smtio.py')
| -rw-r--r-- | backends/smt2/smtio.py | 28 |
1 files changed, 26 insertions, 2 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 497b72db8..dda804efb 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -42,6 +42,7 @@ class SmtModInfo: self.wsize = dict() self.cells = dict() self.asserts = dict() + self.covers = dict() self.anyconsts = dict() @@ -331,6 +332,9 @@ class SmtIo: if fields[1] == "yosys-smt2-assert": self.modinfo[self.curmod].asserts[fields[2]] = fields[3] + if fields[1] == "yosys-smt2-cover": + self.modinfo[self.curmod].covers[fields[2]] = fields[3] + if fields[1] == "yosys-smt2-anyconst": self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3] @@ -567,6 +571,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 +606,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)) |