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

Add proper error message for when smtbmc "append" fails 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-11-04 14:41:28 +01:00
parent 64e0582c29
commit d0acea4f2e
1 changed files with 10 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
backends/smt2/smtbmc.py
View File

@ -1259,7 +1259,11 @@ elif covermode:
smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
smt_assert_consequent(get_constr_expr(constr_assumes, i))
print_msg("Re-solving with appended steps..")
assert smt_check_sat() == "sat"
if smt_check_sat() == "unsat":
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
found_failed_assert = True
retstatus = False
break
reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
assert len(reached_covers) == len(cover_desc)
@ -1377,7 +1381,11 @@ else: # not tempind, covermode
smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
smt_assert_consequent(get_constr_expr(constr_assumes, i))
assert smt_check_sat() == "sat"
print_msg("Re-solving with appended steps..")
if smt_check_sat() == "unsat":
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
retstatus = False
break
print_anyconsts(step)
for i in range(step, last_check_step+1):
print_failed_asserts(i)