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

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 584a1df1a786ba5502f4fe07f9f82466b1bfd516..da65b7bceebe19a8df0be81c239b984acdd4cf42 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -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

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 0e94a1675a9952049d53602f88e8446a5f12806b..cb491b80050e95502f93c5e10321569dc318ea1c 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -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

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 5f93a2fed6e9628760181ad5bd6a160c6e092368..53d2ec57bfdbb105a594dc7906281767f84a4b8b 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -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()):