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

More yosys-smtbmc bugfixes

This commit is contained in:
Clifford Wolf 2016-08-29 14:53:32 +02:00
parent a2e2fc5980
commit b226893461
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
backends/smt2/smtbmc.py
View File

@ -224,10 +224,10 @@ for fn in inconstr:
def get_constr_expr(db, state, final=False, getvalues=False): def get_constr_expr(db, state, final=False, getvalues=False):
if final: if final:
if ("final-%d" % state) not in db: if ("final-%d" % state) not in db:
return "true" return ([], [], []) if getvalues else "true"
else: else:
if state not in db: if state not in db:
return "true" return ([], [], []) if getvalues else "true"
netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)') netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)')
@ -467,14 +467,14 @@ def write_trace(steps):
def print_failed_asserts_worker(mod, state, path): def print_failed_asserts_worker(mod, state, path):
assert mod in smt.modinfo assert mod in smt.modinfo
if smt.get("(|%s_a| s%d)" % (mod, state)) == "true": if smt.get("(|%s_a| %s)" % (mod, state)) == "true":
return return
for cellname, celltype in smt.modinfo[mod].cells.items(): for cellname, celltype in smt.modinfo[mod].cells.items():
print_failed_asserts_worker(celltype, "(|%s_h %s| s%d)" % (mod, cellname, state), path + "." + cellname) print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
for assertfun, assertinfo in smt.modinfo[mod].asserts.items(): for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
if smt.get("(|%s| s%d)" % (assertfun, state)) == "false": if smt.get("(|%s| %s)" % (assertfun, state)) == "false":
print("%s Assert failed in %s: %s" % (smt.timestamp(), path, assertinfo)) print("%s Assert failed in %s: %s" % (smt.timestamp(), path, assertinfo))
@ -486,7 +486,7 @@ def print_failed_asserts(state, final=False):
print("%s Assert %s failed: %s" % (smt.timestamp(), loc, expr)) print("%s Assert %s failed: %s" % (smt.timestamp(), loc, expr))
if not final: if not final:
print_failed_asserts_worker(topmod, state, topmod) print_failed_asserts_worker(topmod, "s%d" % state, topmod)
if tempind: if tempind: