diff options
author | Clifford Wolf <clifford@clifford.at> | 2018-03-05 12:08:41 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2018-03-05 12:17:22 +0100 |
commit | cedbc35f4b4a0244d6499a8a682b42086fb28dfd (patch) | |
tree | d19532fb32ba2773b98d94a42dcdb3527b876777 /backends/smt2 | |
parent | 61a9e2eeb3c67ffb8705e8314d83e3ddacc57645 (diff) | |
download | yosys-cedbc35f4b4a0244d6499a8a682b42086fb28dfd.tar.gz yosys-cedbc35f4b4a0244d6499a8a682b42086fb28dfd.tar.bz2 yosys-cedbc35f4b4a0244d6499a8a682b42086fb28dfd.zip |
Imporove yosys-smtbmc error handling, Improve VCD output
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'backends/smt2')
-rw-r--r-- | backends/smt2/smtbmc.py | 9 | ||||
-rw-r--r-- | backends/smt2/smtio.py | 63 |
2 files changed, 49 insertions, 23 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 70e6ae6fd..6af2a5ac1 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -719,9 +719,12 @@ def write_vlogtb_trace(steps_start, steps_stop, index): if vlogtbtop is not None: for item in vlogtbtop.split("."): - assert item in smt.modinfo[vlogtb_topmod].cells - vlogtb_state = "(|%s_h %s| %s)" % (vlogtb_topmod, item, vlogtb_state) - vlogtb_topmod = smt.modinfo[vlogtb_topmod].cells[item] + if item in smt.modinfo[vlogtb_topmod].cells: + vlogtb_state = "(|%s_h %s| %s)" % (vlogtb_topmod, item, vlogtb_state) + vlogtb_topmod = smt.modinfo[vlogtb_topmod].cells[item] + else: + print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop, item, vlogtb_topmod)) + break with open(filename, "w") as f: print("`ifndef VERILATOR", file=f) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 184a11817..f61f3e77e 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -37,21 +37,30 @@ if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: # currently running solvers (so we can kill them) running_solvers = dict() -got_term_signal = False +forced_shutdown = False solvers_index = 0 -def sig_handler(signum, frame): - global got_term_signal - if not got_term_signal: - print("<%s>" % signal.Signals(signum).name) - got_term_signal = True - for p in running_solvers.values(): - os.killpg(os.getpgid(p.pid), signal.SIGTERM) +def force_shutdown(signum, frame): + global forced_shutdown + if not forced_shutdown: + forced_shutdown = True + if signum is not None: + print("<%s>" % signal.Signals(signum).name) + for p in running_solvers.values(): + # os.killpg(os.getpgid(p.pid), signal.SIGTERM) + os.kill(p.pid, signal.SIGTERM) sys.exit(1) -signal.signal(signal.SIGINT, sig_handler) -signal.signal(signal.SIGHUP, sig_handler) -signal.signal(signal.SIGTERM, sig_handler) +signal.signal(signal.SIGINT, force_shutdown) +signal.signal(signal.SIGHUP, force_shutdown) +signal.signal(signal.SIGTERM, force_shutdown) + +def except_hook(exctype, value, traceback): + if not forced_shutdown: + sys.__excepthook__(exctype, value, traceback) + force_shutdown(None, None) + +sys.excepthook = except_hook hex_dict = { @@ -133,7 +142,7 @@ class SmtIo: self.setup_done = False def __del__(self): - if self.p is not None: + if self.p is not None and not forced_shutdown: os.killpg(os.getpgid(self.p.pid), signal.SIGTERM) if running_solvers is not None: del running_solvers[self.p_index] @@ -948,7 +957,7 @@ class MkVcd: print("b%s %s" % (bits, self.nets[path][0]), file=self.f) def escape_name(self, name): - name = re.sub(r"\[([a-zA-Z_][0-9a-zA-Z_]*)\]", r".\1", name) + name = re.sub(r"\[([0-9a-zA-Z_]*[a-zA-Z_][0-9a-zA-Z_]*)\]", r"<\1>", name) if re.match("[\[\]]", name) and name[0] != "\\": name = "\\" + name return name @@ -959,21 +968,35 @@ class MkVcd: if self.t == -1: print("$var integer 32 t smt_step $end", file=self.f) print("$var event 1 ! smt_clock $end", file=self.f) + scope = [] for path in sorted(self.nets): - while len(scope)+1 > len(path) or (len(scope) > 0 and scope[-1] != path[len(scope)-1]): + key, width = self.nets[path] + + uipath = list(path) + if "." in uipath[-1]: + uipath = uipath[0:-1] + uipath[-1].split(".") + for i in range(len(uipath)): + uipath[i] = re.sub(r"\[([^\]]*)\]", r"<\1>", uipath[i]) + + while uipath[:len(scope)] != scope[:-1]: print("$upscope $end", file=self.f) scope = scope[:-1] - while len(scope)+1 < len(path): - print("$scope module %s $end" % path[len(scope)], file=self.f) - scope.append(path[len(scope)-1]) - key, width = self.nets[path] + print(scope, file=self.f) + + while uipath[:-1] != scope: + print("$scope module %s $end" % uipath[len(scope)], file=self.f) + scope.append(uipath[len(scope)]) + print(scope, file=self.f) + if path in self.clocks and self.clocks[path][1] == "event": - print("$var event 1 %s %s $end" % (key, self.escape_name(path[-1])), file=self.f) + print("$var event 1 %s %s $end" % (key, uipath[-1]), file=self.f) else: - print("$var wire %d %s %s $end" % (width, key, self.escape_name(path[-1])), file=self.f) + print("$var wire %d %s %s $end" % (width, key, uipath[-1]), file=self.f) + for i in range(len(scope)): print("$upscope $end", file=self.f) + print("$enddefinitions $end", file=self.f) self.t = t |