mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 13:29:12 +00:00
Code Activity

Added printing of code loc of failed asserts to yosys-smtbmc

Browse source
This commit is contained in:
Clifford Wolf 2016-08-17 20:10:02 +02:00
parent 42a971226b
commit dfcd30ea86
3 changed files with 23 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
backends/smt2/smt2.cc
View file

@ -605,8 +605,10 @@ struct Smt2Worker
if (cell->type.in("$assert", "$assume")) {
string name_a = get_bool(cell->getPort("\\A"));
string name_en = get_bool(cell->getPort("\\EN"));
decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, log_id(module), idcounter,
cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : log_id(cell)));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell)));
log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell)));
if (cell->type == "$assert")
assert_list.push_back(stringf("(|%s#%d| state)", log_id(module), idcounter++));
else

16
backends/smt2/smtbmc.py
View file

@ -123,6 +123,20 @@ def write_vcd_model(steps):
vcd.set_time(steps)
def print_failed_asserts(mod, state, path):
assert mod in smt.modinfo
if smt.get("(|%s_a| %s)" % (mod, state)) == "true":
return
for cellname, celltype in smt.modinfo[mod].cells.items():
print_failed_asserts(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
if smt.get("(|%s| %s)" % (assertfun, state)) == "false":
print("%s Assert failed in %s: %s" % (smt.timestamp(), path, assertinfo))
if tempind:
retstatus = False
skip_counter = step_size
@ -154,6 +168,7 @@ if tempind:
if smt.check_sat() == "sat":
if step == 0:
print("%s Temporal induction failed!" % smt.timestamp())
print_failed_asserts(topmod, "s%d" % step, topmod)
if vcdfile is not None:
write_vcd_model(num_steps+1)
@ -207,6 +222,7 @@ else: # not tempind
if smt.check_sat() == "sat":
print("%s BMC failed!" % smt.timestamp())
print_failed_asserts(topmod, "s%d" % step, topmod)
if vcdfile is not None:
write_vcd_model(step+step_size)
retstatus = False

4
backends/smt2/smtio.py
View file

@ -30,6 +30,7 @@ class smtmodinfo:
self.wires = set()
self.wsize = dict()
self.cells = dict()
self.asserts = dict()
class smtio:
def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
@ -129,6 +130,9 @@ class smtio:
self.modinfo[self.curmod].wires.add(fields[2])
self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
if fields[1] == "yosys-smt2-assert":
self.modinfo[self.curmod].asserts[fields[2]] = fields[3]
def hiernets(self, top):
def hiernets_worker(nets, mod, cursor):
for netname in sorted(self.modinfo[mod].wsize.keys()):