diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smtbmc.py | 28 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 15 |
2 files changed, 23 insertions, 20 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 445a42e0d..3d6d3e1b3 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1256,7 +1256,7 @@ def smt_check_sat(): return smt.check_sat() if tempind: - retstatus = False + retstatus = "FAILED" skip_counter = step_size for step in range(num_steps, -1, -1): if smt.forall: @@ -1303,7 +1303,7 @@ if tempind: else: print_msg("Temporal induction successful.") - retstatus = True + retstatus = "PASSED" break elif covermode: @@ -1321,7 +1321,7 @@ elif covermode: smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr)) step = 0 - retstatus = False + retstatus = "FAILED" found_failed_assert = False assert step_size == 1 @@ -1365,7 +1365,7 @@ elif covermode: if smt_check_sat() == "unsat": print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) found_failed_assert = True - retstatus = False + retstatus = "FAILED" break reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step))) @@ -1400,7 +1400,7 @@ elif covermode: break if "1" not in cover_mask: - retstatus = True + retstatus = "PASSED" break step += 1 @@ -1412,7 +1412,7 @@ elif covermode: else: # not tempind, covermode step = 0 - retstatus = True + retstatus = "PASSED" while step < num_steps: smt_state(step) smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) @@ -1459,8 +1459,8 @@ else: # not tempind, covermode print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step)) if smt_check_sat() == "unsat": - print("%s Warmup failed!" % smt.timestamp()) - retstatus = False + print("%s Assumptions are unsatisfiable!" % smt.timestamp()) + retstatus = "PREUNSAT" break if not final_only: @@ -1487,13 +1487,13 @@ else: # not tempind, covermode print_msg("Re-solving with appended steps..") if smt_check_sat() == "unsat": print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) - retstatus = False + retstatus = "FAILED" break print_anyconsts(step) for i in range(step, last_check_step+1): print_failed_asserts(i) write_trace(0, last_check_step+1+append_steps, '%') - retstatus = False + retstatus = "FAILED" break smt_pop() @@ -1519,7 +1519,7 @@ else: # not tempind, covermode print_anyconsts(i) print_failed_asserts(i, final=True) write_trace(0, i+1, '%') - retstatus = False + retstatus = "FAILED" break smt_pop() @@ -1534,7 +1534,7 @@ else: # not tempind, covermode print_msg("Solving for step %d.." % (last_check_step)) if smt_check_sat() != "sat": print("%s No solution found!" % smt.timestamp()) - retstatus = False + retstatus = "FAILED" break elif dumpall: @@ -1551,5 +1551,5 @@ else: # not tempind, covermode smt.write("(exit)") smt.wait() -print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)")) -sys.exit(0 if retstatus else 1) +print_msg("Status: %s" % retstatus) +sys.exit(0 if retstatus == "PASSED" else 1) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index bac68ac70..1df996aa7 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -1032,12 +1032,17 @@ class MkVcd: print("$var integer 32 t smt_step $end", file=self.f) print("$var event 1 ! smt_clock $end", file=self.f) + def vcdescape(n): + if n.startswith("$") or ":" in n: + return "\\" + n + return n + scope = [] for path in sorted(self.nets): key, width = self.nets[path] uipath = list(path) - if "." in uipath[-1]: + if "." in uipath[-1] and not uipath[-1].startswith("$"): uipath = uipath[0:-1] + uipath[-1].split(".") for i in range(len(uipath)): uipath[i] = re.sub(r"\[([^\]]*)\]", r"<\1>", uipath[i]) @@ -1048,15 +1053,13 @@ class MkVcd: while uipath[:-1] != scope: scopename = uipath[len(scope)] - if scopename.startswith("$"): - scopename = "\\" + scopename - print("$scope module %s $end" % scopename, file=self.f) + print("$scope module %s $end" % vcdescape(scopename), file=self.f) scope.append(uipath[len(scope)]) if path in self.clocks and self.clocks[path][1] == "event": - print("$var event 1 %s %s $end" % (key, uipath[-1]), file=self.f) + print("$var event 1 %s %s $end" % (key, vcdescape(uipath[-1])), file=self.f) else: - print("$var wire %d %s %s $end" % (width, key, uipath[-1]), file=self.f) + print("$var wire %d %s %s $end" % (width, key, vcdescape(uipath[-1])), file=self.f) for i in range(len(scope)): print("$upscope $end", file=self.f) |