include memory in state

backends/smt2/smtbmc.py

@@ -55,7 +55,7 @@ noinit = False
 binarymode = False
 keep_going = False
 check_witness = False
-find_loops = False
+detect_loops = False
 so = SmtOpts()
 
 
@@ -176,8 +176,9 @@ def usage():
         check that the used witness file contains sufficient
         constraints to force an assertion failure.
 
-    --find-loops
-        check if states are unique in temporal induction counterexamples
+    --detect-loops
+        check if states are unique in temporal induction counter examples
+        (this feature is experimental and incomplete)
 
 """ + so.helpmsg())
     sys.exit(1)
@@ -187,7 +188,7 @@ try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
             ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat",
              "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
-             "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "find-loops"])
+             "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"])
 except:
     usage()
 
@@ -268,8 +269,8 @@ for o, a in opts:
         keep_going = True
     elif o == "--check-witness":
         check_witness = True
-    elif o == "--find-loops":
-        find_loops = True
+    elif o == "--detect-loops":
+        detect_loops = True
     elif so.handle(o, a):
         pass
     else:
@@ -975,36 +976,29 @@ def write_vcd_trace(steps_start, steps_stop, index):
 
         vcd.set_time(steps_stop)
 
-def find_state_loop(steps_start, steps_stop):
-    print_msg(f"Looking for loops")
+def detect_state_loop(steps_start, steps_stop):
+    print_msg(f"Checking for loops in found induction counter example")
+    print_msg(f"This feature is experimental and incomplete")
 
-    path_list = list()
-
-    for netpath in sorted(smt.hiernets(topmod)):
-        hidden_net = False
-        for n in netpath:
-            if n.startswith("$"):
-                hidden_net = True
-        if not hidden_net:
-            path_list.append(netpath)
+    path_list = sorted(smt.hiernets(topmod, regs_only=True))
 
     mem_trace_data = collect_mem_trace_data(steps_start, steps_stop)
 
+    # Map state to index of step when it occurred
     states = dict()
-    path_tupled_list = [tuple(p) for p in path_list]
+
     for i in range(steps_start, steps_stop):
         value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
-        state = tuple(zip(path_tupled_list, value_list))
+        mem_state = sorted(
+            [(tuple(path), addr, data)
+             for path, addr, data in mem_trace_data.get(i, [])]
+        )
+        state = tuple(value_list), tuple(mem_state)
         if states.get(state):
             return (i, states[state])
         else:
             states[state] = i
 
-        if i in mem_trace_data:
-            if mem_trace_data[i]:
-                print_msg(f"This design contains memory. Searching for counterexample loops will be skipped")
-                return None
-
     return None
 
 def char_ok_in_verilog(c,i):
@@ -1634,10 +1628,10 @@ if tempind:
                 print_anyconsts(num_steps)
                 print_failed_asserts(num_steps)
                 write_trace(step, num_steps+1, '%', allregs=True)
-                if find_loops:
-                    loop = find_state_loop(step, num_steps+1)
+                if detect_loops:
+                    loop = detect_state_loop(step, num_steps+1)
                     if loop:
-                        print_msg(f"Loop detected, increasing induction depth will not help. Cycle {loop[0]} = cycle {loop[1]}")
+                        print_msg(f"Loop detected, increasing induction depth will not help. Step {loop[0]} = step {loop[1]}")
 
             elif dumpall:
                 print_anyconsts(num_steps)