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

Change smtbmc "Warmup failed" status to "PREUNSAT" 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2019-10-03 14:59:07 +02:00
parent 17cb916cc8
commit 2ed2e9c3e8
1 changed files with 14 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
backends/smt2/smtbmc.py
View File

@ -1256,7 +1256,7 @@ def smt_check_sat():
return smt.check_sat() return smt.check_sat()
if tempind: if tempind:
retstatus = False retstatus = "FAILED"
skip_counter = step_size skip_counter = step_size
for step in range(num_steps, -1, -1): for step in range(num_steps, -1, -1):
if smt.forall: if smt.forall:
@ -1303,7 +1303,7 @@ if tempind:
else: else:
print_msg("Temporal induction successful.") print_msg("Temporal induction successful.")
retstatus = True retstatus = "PASSED"
break break
elif covermode: 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)) smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
step = 0 step = 0
retstatus = False retstatus = "FAILED"
found_failed_assert = False found_failed_assert = False
assert step_size == 1 assert step_size == 1
@ -1365,7 +1365,7 @@ elif covermode:
if smt_check_sat() == "unsat": if smt_check_sat() == "unsat":
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
found_failed_assert = True found_failed_assert = True
retstatus = False retstatus = "FAILED"
break break
reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step))) reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
@ -1400,7 +1400,7 @@ elif covermode:
break break
if "1" not in cover_mask: if "1" not in cover_mask:
retstatus = True retstatus = "PASSED"
break break
step += 1 step += 1
@ -1412,7 +1412,7 @@ elif covermode:
else: # not tempind, covermode else: # not tempind, covermode
step = 0 step = 0
retstatus = True retstatus = "PASSED"
while step < num_steps: while step < num_steps:
smt_state(step) smt_state(step)
smt_assert_consequent("(|%s_u| s%d)" % (topmod, 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)) print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
if smt_check_sat() == "unsat": if smt_check_sat() == "unsat":
print("%s Warmup failed!" % smt.timestamp()) print("%s Assumptions are unsatisfiable!" % smt.timestamp())
retstatus = False retstatus = "PREUNSAT"
break break
if not final_only: if not final_only:
@ -1487,13 +1487,13 @@ else: # not tempind, covermode
print_msg("Re-solving with appended steps..") print_msg("Re-solving with appended steps..")
if smt_check_sat() == "unsat": if smt_check_sat() == "unsat":
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
retstatus = False retstatus = "FAILED"
break break
print_anyconsts(step) print_anyconsts(step)
for i in range(step, last_check_step+1): for i in range(step, last_check_step+1):
print_failed_asserts(i) print_failed_asserts(i)
write_trace(0, last_check_step+1+append_steps, '%') write_trace(0, last_check_step+1+append_steps, '%')
retstatus = False retstatus = "FAILED"
break break
smt_pop() smt_pop()
@ -1519,7 +1519,7 @@ else: # not tempind, covermode
print_anyconsts(i) print_anyconsts(i)
print_failed_asserts(i, final=True) print_failed_asserts(i, final=True)
write_trace(0, i+1, '%') write_trace(0, i+1, '%')
retstatus = False retstatus = "FAILED"
break break
smt_pop() smt_pop()
@ -1534,7 +1534,7 @@ else: # not tempind, covermode
print_msg("Solving for step %d.." % (last_check_step)) print_msg("Solving for step %d.." % (last_check_step))
if smt_check_sat() != "sat": if smt_check_sat() != "sat":
print("%s No solution found!" % smt.timestamp()) print("%s No solution found!" % smt.timestamp())
retstatus = False retstatus = "FAILED"
break break
elif dumpall: elif dumpall:
@ -1551,5 +1551,5 @@ else: # not tempind, covermode
smt.write("(exit)") smt.write("(exit)")
smt.wait() smt.wait()
print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)")) print_msg("Status: %s" % retstatus)
sys.exit(0 if retstatus else 1) sys.exit(0 if retstatus == "PASSED" else 1)