aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2017-10-25 19:59:56 +0200
committerClifford Wolf <clifford@clifford.at>2017-10-25 19:59:56 +0200
commitf513494f5fabd2596b1748cf67dcaf70723b28f7 (patch)
treef2e672e0ca67a31483df72eb8bf3837e523754fe /backends/smt2
parent76326c163a6698ab33059ca5fcf34b5e46bb8538 (diff)
downloadyosys-f513494f5fabd2596b1748cf67dcaf70723b28f7.tar.gz
yosys-f513494f5fabd2596b1748cf67dcaf70723b28f7.tar.bz2
yosys-f513494f5fabd2596b1748cf67dcaf70723b28f7.zip
Use separate writer thread for talking to SMT solver to avoid read/write deadlock
Diffstat (limited to 'backends/smt2')
-rw-r--r--backends/smt2/smtio.py31
1 files changed, 23 insertions, 8 deletions
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: