Added $anyconst support to yosys-smtbmc

3 files changed, 27 insertions, 1 deletions

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9668a6425..30a6bb19c 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -420,6 +420,8 @@ struct Smt2Worker
 			if (cell->type == "$anyconst")
 			{
 				registers.insert(cell);
+				decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
+						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
 				decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
 						get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))));
 				register_bv(cell->getPort("\\Y"), idcounter++);
@@ -669,7 +671,7 @@ struct Smt2Worker
 				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, get_id(module), idcounter,
-					cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
 				decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
 						get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
 				if (cell->type == "$assert")
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 9096654f0..fa887dd15 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -504,6 +504,20 @@ def print_failed_asserts(state, final=False):
         print_failed_asserts_worker(topmod, "s%d" % state, topmod)
 
 
+def print_anyconsts_worker(mod, state, path):
+    assert mod in smt.modinfo
+
+    for cellname, celltype in smt.modinfo[mod].cells.items():
+        print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
+
+    for fun, info in smt.modinfo[mod].anyconsts.items():
+        print("%s Value for anyconst in %s (%s): %d" % (smt.timestamp(), path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+
+
+def print_anyconsts(state):
+    print_anyconsts_worker(topmod, "s%d" % state, topmod)
+
+
 if tempind:
     retstatus = False
     skip_counter = step_size
@@ -535,10 +549,12 @@ if tempind:
         if smt.check_sat() == "sat":
             if step == 0:
                 print("%s Temporal induction failed!" % smt.timestamp())
+                print_anyconsts(num_steps)
                 print_failed_asserts(num_steps)
                 write_trace(step, num_steps+1, '%')
 
             elif dumpall:
+                print_anyconsts(num_steps)
                 print_failed_asserts(num_steps)
                 write_trace(step, num_steps+1, "%d" % step)
 
@@ -598,6 +614,7 @@ else: # not tempind
 
                 if smt.check_sat() == "sat":
                     print("%s BMC failed!" % smt.timestamp())
+                    print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)
                     write_trace(0, last_check_step+1, '%')
@@ -623,6 +640,7 @@ else: # not tempind
 
                     if smt.check_sat() == "sat":
                         print("%s BMC failed!" % smt.timestamp())
+                        print_anyconsts(i)
                         print_failed_asserts(i, final=True)
                         write_trace(0, i+1, '%')
                         retstatus = False
@@ -644,11 +662,13 @@ else: # not tempind
                 break
 
             elif dumpall:
+                print_anyconsts(0)
                 write_trace(0, last_check_step+1, "%d" % step)
 
         step += step_size
 
     if gentrace:
+        print_anyconsts(0)
         write_trace(0, num_steps, '%')
 
 
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index da9d4830f..fc7d1e13d 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -32,6 +32,7 @@ class smtmodinfo:
         self.wsize = dict()
         self.cells = dict()
         self.asserts = dict()
+        self.anyconsts = dict()
 
 class smtio:
     def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
@@ -137,6 +138,9 @@ class smtio:
         if fields[1] == "yosys-smt2-assert":
             self.modinfo[self.curmod].asserts[fields[2]] = fields[3]
 
+        if fields[1] == "yosys-smt2-anyconst":
+            self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3]
+
     def hiernets(self, top, regs_only=False):
         def hiernets_worker(nets, mod, cursor):
             for netname in sorted(self.modinfo[mod].wsize.keys()):