diff options
Diffstat (limited to 'backends/smt2/smtio.py')
| -rw-r--r-- | backends/smt2/smtio.py | 97 |
1 files changed, 82 insertions, 15 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 91efc13a3..a73745896 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -16,7 +16,7 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import sys, re, os, signal +import sys, re, os, signal, json import subprocess if os.name == "posix": import resource @@ -108,6 +108,7 @@ class SmtModInfo: self.allconsts = dict() self.allseqs = dict() self.asize = dict() + self.witness = [] class SmtIo: @@ -337,7 +338,7 @@ class SmtIo: def p_thread_main(self): while True: - data = self.p.stdout.readline().decode("ascii") + data = self.p.stdout.readline().decode("utf-8") if data == "": break self.p_queue.put(data) self.p_queue.put("") @@ -359,7 +360,7 @@ class SmtIo: def p_write(self, data, flush): assert self.p is not None - self.p.stdin.write(bytes(data, "ascii")) + self.p.stdin.write(bytes(data, "utf-8")) if flush: self.p.stdin.flush() def p_read(self): @@ -587,6 +588,11 @@ class SmtIo: self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5]) self.modinfo[self.curmod].asize[fields[2]] = int(fields[3]) + if fields[1] == "yosys-smt2-witness": + data = json.loads(stmt.split(None, 2)[2]) + if data.get("type") in ["cell", "mem", "posedge", "negedge", "input", "reg", "init", "seq", "blackbox"]: + self.modinfo[self.curmod].witness.append(data) + def hiernets(self, top, regs_only=False): def hiernets_worker(nets, mod, cursor): for netname in sorted(self.modinfo[mod].wsize.keys()): @@ -658,6 +664,57 @@ class SmtIo: hiermems_worker(mems, top, []) return mems + def hierwitness(self, top, allregs=False, blackbox=True): + init_witnesses = [] + seq_witnesses = [] + clk_witnesses = [] + mem_witnesses = [] + + def absolute(path, cursor, witness): + return { + **witness, + "path": path + tuple(witness["path"]), + "smtpath": cursor + [witness["smtname"]], + } + + for witness in self.modinfo[top].witness: + if witness["type"] == "input": + seq_witnesses.append(absolute((), [], witness)) + if witness["type"] in ("posedge", "negedge"): + clk_witnesses.append(absolute((), [], witness)) + + init_types = ["init"] + if allregs: + init_types.append("reg") + + seq_types = ["seq"] + if blackbox: + seq_types.append("blackbox") + + def worker(mod, path, cursor): + cell_paths = {} + for witness in self.modinfo[mod].witness: + if witness["type"] in init_types: + init_witnesses.append(absolute(path, cursor, witness)) + if witness["type"] in seq_types: + seq_witnesses.append(absolute(path, cursor, witness)) + if witness["type"] == "mem": + if allregs and not witness["rom"]: + width, size = witness["width"], witness["size"] + witness = {**witness, "uninitialized": [{"width": width * size, "offset": 0}]} + if not witness["uninitialized"]: + continue + + mem_witnesses.append(absolute(path, cursor, witness)) + if witness["type"] == "cell": + cell_paths[witness["smtname"]] = tuple(witness["path"]) + + for cellname, celltype in sorted(self.modinfo[mod].cells.items()): + worker(celltype, path + cell_paths.get(cellname, ("?" + cellname,)), cursor + [cellname]) + + worker(top, (), []) + return init_witnesses, seq_witnesses, clk_witnesses, mem_witnesses + def read(self): stmt = [] count_brackets = 0 @@ -790,31 +847,28 @@ class SmtIo: return result def parse(self, stmt): - def worker(stmt): - if stmt[0] == '(': + def worker(stmt, cursor=0): + while stmt[cursor] in [" ", "\t", "\r", "\n"]: + cursor += 1 + + if stmt[cursor] == '(': expr = [] - cursor = 1 + cursor += 1 while stmt[cursor] != ')': - el, le = worker(stmt[cursor:]) + el, cursor = worker(stmt, cursor) expr.append(el) - cursor += le return expr, cursor+1 - if stmt[0] == '|': + if stmt[cursor] == '|': expr = "|" - cursor = 1 + cursor += 1 while stmt[cursor] != '|': expr += stmt[cursor] cursor += 1 expr += "|" return expr, cursor+1 - if stmt[0] in [" ", "\t", "\r", "\n"]: - el, le = worker(stmt[1:]) - return el, le+1 - expr = "" - cursor = 0 while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]: expr += stmt[cursor] cursor += 1 @@ -887,6 +941,8 @@ class SmtIo: assert mod in self.modinfo if path[0] == "": return base + if isinstance(path[0], int): + return "(|%s#%d| %s)" % (mod, path[0], base) if path[0] in self.modinfo[mod].cells: return "(|%s_h %s| %s)" % (mod, path[0], base) if path[0] in self.modinfo[mod].wsize: @@ -902,6 +958,15 @@ class SmtIo: nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) return self.net_expr(nextmod, nextbase, path[1:]) + def witness_net_expr(self, mod, base, witness): + net = self.net_expr(mod, base, witness["smtpath"]) + is_bool = self.net_width(mod, witness["smtpath"]) == 1 + if is_bool: + assert witness["width"] == 1 + assert witness["smtoffset"] == 0 + return net + return "((_ extract %d %d) %s)" % (witness["smtoffset"] + witness["width"] - 1, witness["smtoffset"], net) + def net_width(self, mod, net_path): for i in range(len(net_path)-1): assert mod in self.modinfo @@ -909,6 +974,8 @@ class SmtIo: mod = self.modinfo[mod].cells[net_path[i]] assert mod in self.modinfo + if isinstance(net_path[-1], int): + return None assert net_path[-1] in self.modinfo[mod].wsize return self.modinfo[mod].wsize[net_path[-1]] |