From dd46d76394eb3f345d8af63ade4fd2b4f2e443e1 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 13:05:14 +0200 Subject: Fix a bug in yosys-smtbmc in ROM handling --- backends/smt2/smtbmc.py | 3 +++ 1 file changed, 3 insertions(+) (limited to 'backends') 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)): -- cgit v1.2.3 From c672c321e3cca1803e5f1108d3438e9e18800635 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 13:37:11 +0200 Subject: Capsulate smt-solver read/write in separate functions --- backends/smt2/smtio.py | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index abf8e812d..7cd7d0d59 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -58,6 +58,7 @@ class SmtIo: self.produce_models = True self.smt2cache = [list()] self.p = None + self.p_buffer = [] if opts is not None: self.logic = opts.logic @@ -209,6 +210,19 @@ class SmtIo: return stmt + def p_write(self, data): + # select_result = select([self.p.stdout], [self.p.stdin], [], 0.1): + wlen = self.p.stdin.write(data) + assert wlen == len(data) + + def p_flush(self): + self.p.stdin.flush() + + def p_read(self): + if len(self.p_buffer) == 0: + return self.p.stdout.readline().decode("ascii") + assert 0 + def write(self, stmt, unroll=True): if stmt.startswith(";"): self.info(stmt) @@ -283,18 +297,19 @@ class SmtIo: if self.p is not None and not stmt.startswith("(get-"): self.p.stdin.close() self.p = None + self.p_buffer = [] 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(bytes(stmt + "\n", "ascii")) + self.p_flush() self.smt2cache[-1].append(stmt) else: - self.p.stdin.write(bytes(stmt + "\n", "ascii")) - self.p.stdin.flush() + self.p_write(bytes(stmt + "\n", "ascii")) + self.p_flush() def info(self, stmt): if not stmt.startswith("; yosys-smt2-"): @@ -408,7 +423,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") @@ -443,13 +458,14 @@ class SmtIo: if self.p is not None: self.p.stdin.close() self.p = None + self.p_buffer = [] self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) for cache_ctx in self.smt2cache: for cache_stmt in cache_ctx: - self.p.stdin.write(bytes(cache_stmt + "\n", "ascii")) + self.p_write(bytes(cache_stmt + "\n", "ascii")) - self.p.stdin.write(bytes("(check-sat)\n", "ascii")) - self.p.stdin.flush() + self.p_write(bytes("(check-sat)\n", "ascii")) + self.p_flush() if self.timeinfo: i = 0 -- cgit v1.2.3 From 76326c163a6698ab33059ca5fcf34b5e46bb8538 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 15:45:32 +0200 Subject: Improve p_* functions in smtio.py --- backends/smt2/smtio.py | 40 +++++++++++++++++++--------------------- 1 file changed, 19 insertions(+), 21 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 7cd7d0d59..18dee4e95 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -127,7 +127,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 @@ -210,19 +210,24 @@ class SmtIo: return stmt - def p_write(self, data): - # select_result = select([self.p.stdout], [self.p.stdin], [], 0.1): - wlen = self.p.stdin.write(data) - assert wlen == len(data) + def p_open(self): + self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - def p_flush(self): - self.p.stdin.flush() + def p_write(self, data, flush): + self.p.stdin.write(bytes(data, "ascii")) + if flush: + self.p.stdin.flush() def p_read(self): if len(self.p_buffer) == 0: return self.p.stdout.readline().decode("ascii") assert 0 + def p_close(self): + self.p.stdin.close() + self.p = None + self.p_buffer = [] + def write(self, stmt, unroll=True): if stmt.startswith(";"): self.info(stmt) @@ -295,21 +300,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_buffer = [] + 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_write(bytes(stmt + "\n", "ascii")) - self.p_flush() + self.p_write(stmt + "\n", True) self.smt2cache[-1].append(stmt) else: - self.p_write(bytes(stmt + "\n", "ascii")) - self.p_flush() + self.p_write(stmt + "\n", True) def info(self, stmt): if not stmt.startswith("; yosys-smt2-"): @@ -456,16 +457,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_buffer = [] - 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_write(bytes(cache_stmt + "\n", "ascii")) + self.p_write(cache_stmt + "\n", False) - self.p_write(bytes("(check-sat)\n", "ascii")) - self.p_flush() + self.p_write("(check-sat)\n", True) if self.timeinfo: i = 0 -- cgit v1.2.3 From f513494f5fabd2596b1748cf67dcaf70723b28f7 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 25 Oct 2017 19:59:56 +0200 Subject: Use separate writer thread for talking to SMT solver to avoid read/write deadlock --- backends/smt2/smtio.py | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 18dee4e95..6e7b68242 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 +from threading import Thread hex_dict = { @@ -58,7 +60,6 @@ class SmtIo: self.produce_models = True self.smt2cache = [list()] self.p = None - self.p_buffer = [] if opts is not None: self.logic = opts.logic @@ -210,23 +211,36 @@ class SmtIo: return stmt + def p_thread_main(self): + while True: + data = self.p_queue.get() + if data is None: break + self.p.stdin.write(data[0]) + if data[1]: self.p.stdin.flush() + 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_queue = Queue() + self.p_thread = Thread(target=self.p_thread_main) + self.p_thread.start() def p_write(self, data, flush): - self.p.stdin.write(bytes(data, "ascii")) - if flush: - self.p.stdin.flush() + assert self.p is not None + self.p_queue.put((bytes(data, "ascii"), flush)) def p_read(self): - if len(self.p_buffer) == 0: - return self.p.stdout.readline().decode("ascii") - assert 0 + assert self.p is not None + return self.p.stdout.readline().decode("ascii") def p_close(self): + assert self.p is not None + self.p_queue.put(None) + self.p_thread.join() self.p.stdin.close() self.p = None - self.p_buffer = [] + self.p_queue = None + self.p_thread = None def write(self, stmt, unroll=True): if stmt.startswith(";"): @@ -686,6 +700,7 @@ class SmtIo: def wait(self): if self.p is not None: self.p.wait() + self.p_close() class SmtOpts: -- cgit v1.2.3 From 11705082648143c8be1a8b8fd4ef60ee81451c01 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 26 Oct 2017 01:01:55 +0200 Subject: Improve smtio performance by using reader thread, not writer thread --- backends/smt2/smtio.py | 40 ++++++++++++++++++++++++++++++---------- 1 file changed, 30 insertions(+), 10 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 6e7b68242..61ac14c82 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -20,7 +20,7 @@ import sys, subprocess, re, os from copy import deepcopy from select import select from time import time -from queue import Queue +from queue import Queue, Empty from threading import Thread @@ -213,32 +213,52 @@ class SmtIo: def p_thread_main(self): while True: - data = self.p_queue.get() - if data is None: break - self.p.stdin.write(data[0]) - if data[1]: self.p.stdin.flush() + 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_queue.put((bytes(data, "ascii"), flush)) + self.p.stdin.write(bytes(data, "ascii")) + if flush: self.p.stdin.flush() def p_read(self): assert self.p is not None - return self.p.stdout.readline().decode("ascii") + 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_queue.put(None) - self.p_thread.join() 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 @@ -485,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: -- cgit v1.2.3 From 455c1c9d97330b9d20cafe62cd72c3c3f71d3573 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 29 Oct 2017 13:21:20 +0100 Subject: Fix SMT2 handling of initstate in sub-modules --- backends/smt2/smt2.cc | 3 +++ 1 file changed, 3 insertions(+) (limited to 'backends') 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); -- cgit v1.2.3