diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smt2.cc | 3 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 3 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 79 |
3 files changed, 70 insertions, 15 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index dce7c25de..8daa52eb3 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -811,6 +811,9 @@ struct Smt2Worker Module *m = module->design->module(cell->type); log_assert(m != nullptr); + hier.push_back(stringf(" (= (|%s_is| state) (|%s_is| %s))\n", + get_id(module), get_id(cell->type), cell_state.c_str())); + for (auto &conn : cell->connections()) { Wire *w = m->wire(conn.first); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index c8151c266..d9b79e26e 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -644,6 +644,9 @@ def write_vcd_trace(steps_start, steps_stop, index): data = ["x"] * width gotread = False + if len(wdata) == 0 and len(rdata) != 0: + wdata = [[]] * len(rdata) + assert len(rdata) == len(wdata) for i in range(len(wdata)): diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index abf8e812d..61ac14c82 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -20,6 +20,8 @@ import sys, subprocess, re, os from copy import deepcopy from select import select from time import time +from queue import Queue, Empty +from threading import Thread hex_dict = { @@ -126,7 +128,7 @@ class SmtIo: if self.dummy_file is not None: self.dummy_fd = open(self.dummy_file, "w") if not self.noincr: - self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + self.p_open() if self.unroll: self.logic_uf = False @@ -209,6 +211,57 @@ class SmtIo: return stmt + def p_thread_main(self): + while True: + data = self.p.stdout.readline().decode("ascii") + if data == "": break + self.p_queue.put(data) + self.p_running = False + + def p_open(self): + assert self.p is None + self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + self.p_running = True + self.p_next = None + self.p_queue = Queue() + self.p_thread = Thread(target=self.p_thread_main) + self.p_thread.start() + + def p_write(self, data, flush): + assert self.p is not None + self.p.stdin.write(bytes(data, "ascii")) + if flush: self.p.stdin.flush() + + def p_read(self): + assert self.p is not None + assert self.p_running + if self.p_next is not None: + data = self.p_next + self.p_next = None + return data + return self.p_queue.get() + + def p_poll(self): + assert self.p is not None + assert self.p_running + if self.p_next is not None: + return False + try: + self.p_next = self.p_queue.get(True, 0.1) + return False + except Empty: + return True + + def p_close(self): + assert self.p is not None + self.p.stdin.close() + self.p_thread.join() + assert not self.p_running + self.p = None + self.p_next = None + self.p_queue = None + self.p_thread = None + def write(self, stmt, unroll=True): if stmt.startswith(";"): self.info(stmt) @@ -281,20 +334,17 @@ class SmtIo: if self.solver != "dummy": if self.noincr: if self.p is not None and not stmt.startswith("(get-"): - self.p.stdin.close() - self.p = None + self.p_close() if stmt == "(push 1)": self.smt2cache.append(list()) elif stmt == "(pop 1)": self.smt2cache.pop() else: if self.p is not None: - self.p.stdin.write(bytes(stmt + "\n", "ascii")) - self.p.stdin.flush() + self.p_write(stmt + "\n", True) self.smt2cache[-1].append(stmt) else: - self.p.stdin.write(bytes(stmt + "\n", "ascii")) - self.p.stdin.flush() + self.p_write(stmt + "\n", True) def info(self, stmt): if not stmt.startswith("; yosys-smt2-"): @@ -408,7 +458,7 @@ class SmtIo: if self.solver == "dummy": line = self.dummy_fd.readline().strip() else: - line = self.p.stdout.readline().decode("ascii").strip() + line = self.p_read().strip() if self.dummy_file is not None: self.dummy_fd.write(line + "\n") @@ -441,15 +491,13 @@ class SmtIo: if self.solver != "dummy": if self.noincr: if self.p is not None: - self.p.stdin.close() - self.p = None - self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + self.p_close() + self.p_open() for cache_ctx in self.smt2cache: for cache_stmt in cache_ctx: - self.p.stdin.write(bytes(cache_stmt + "\n", "ascii")) + self.p_write(cache_stmt + "\n", False) - self.p.stdin.write(bytes("(check-sat)\n", "ascii")) - self.p.stdin.flush() + self.p_write("(check-sat)\n", True) if self.timeinfo: i = 0 @@ -457,7 +505,7 @@ class SmtIo: count = 0 num_bs = 0 - while select([self.p.stdout], [], [], 0.1) == ([], [], []): + while self.p_poll(): count += 1 if count < 25: @@ -672,6 +720,7 @@ class SmtIo: def wait(self): if self.p is not None: self.p.wait() + self.p_close() class SmtOpts: |