riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Improve yosys-smtbmc log output and error handling 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-17 18:06:17 +01:00
parent 4d4e3a8ca6
commit 3f00702475
1 changed files with 14 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
backends/smt2/smtio.py
View File

@ -218,7 +218,7 @@ class SmtIo:
def timestamp(self): def timestamp(self):
secs = int(time() - self.start_time) secs = int(time() - self.start_time)
return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60) return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)
def replace_in_stmt(self, stmt, pat, repl): def replace_in_stmt(self, stmt, pat, repl):
if stmt == pat: if stmt == pat:
@ -294,11 +294,12 @@ class SmtIo:
def p_read(self): def p_read(self):
assert self.p is not None assert self.p is not None
assert self.p_running
if self.p_next is not None: if self.p_next is not None:
data = self.p_next data = self.p_next
self.p_next = None self.p_next = None
return data return data
if not self.p_running:
return ""
return self.p_queue.get() return self.p_queue.get()
def p_poll(self): def p_poll(self):
@ -580,12 +581,12 @@ class SmtIo:
if count_brackets == 0: if count_brackets == 0:
break break
if self.solver != "dummy" and self.p.poll(): if self.solver != "dummy" and self.p.poll():
print("SMT Solver terminated unexpectedly: %s" % "".join(stmt), flush=True) print("%s Solver terminated unexpectedly: %s" % (self.timestamp(), "".join(stmt)), flush=True)
sys.exit(1) sys.exit(1)
stmt = "".join(stmt) stmt = "".join(stmt)
if stmt.startswith("(error"): if stmt.startswith("(error"):
print("SMT Solver Error: %s" % stmt, file=sys.stderr, flush=True) print("%s Solver Error: %s" % (self.timestamp(), stmt), flush=True)
if self.solver != "dummy": if self.solver != "dummy":
self.p_close() self.p_close()
sys.exit(1) sys.exit(1)
@ -652,7 +653,15 @@ class SmtIo:
print("(check-sat)", file=self.debug_file) print("(check-sat)", file=self.debug_file)
self.debug_file.flush() self.debug_file.flush()
assert result in ["sat", "unsat"] if result not in ["sat", "unsat"]:
if result == "":
print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
else:
print("%s Unexpected response from solver: %s" % (self.timestamp(), result), flush=True)
if self.solver != "dummy":
self.p_close()
sys.exit(1)
return result return result
def parse(self, stmt): def parse(self, stmt):