Temporal induction counterexample loop detection (#3504)

I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties.

1 files changed, 36 insertions, 1 deletions

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index ac329053f..4c1f07229 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -55,6 +55,7 @@ noinit = False
 binarymode = False
 keep_going = False
 check_witness = False
+detect_loops = False
 so = SmtOpts()
 
 
@@ -175,6 +176,10 @@ def usage():
         check that the used witness file contains sufficient
         constraints to force an assertion failure.
 
+    --detect-loops
+        check if states are unique in temporal induction counter examples
+        (this feature is experimental and incomplete)
+
 """ + so.helpmsg())
     sys.exit(1)
 
@@ -183,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"])
+             "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"])
 except:
     usage()
 
@@ -264,6 +269,8 @@ for o, a in opts:
         keep_going = True
     elif o == "--check-witness":
         check_witness = True
+    elif o == "--detect-loops":
+        detect_loops = True
     elif so.handle(o, a):
         pass
     else:
@@ -969,6 +976,30 @@ def write_vcd_trace(steps_start, steps_stop, index):
 
         vcd.set_time(steps_stop)
 
+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 = 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()
+
+    for i in range(steps_start, steps_stop):
+        value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
+        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 state in states:
+            return (i, states[state])
+        else:
+            states[state] = i
+
+    return None
+
 def char_ok_in_verilog(c,i):
     if ('A' <= c <= 'Z'): return True
     if ('a' <= c <= 'z'): return True
@@ -1597,6 +1628,10 @@ if tempind:
                 print_anyconsts(num_steps)
                 print_failed_asserts(num_steps)
                 write_trace(step, num_steps+1, '%', allregs=True)
+                if detect_loops:
+                    loop = detect_state_loop(step, num_steps+1)
+                    if loop:
+                        print_msg(f"Loop detected, increasing induction depth will not help. Step {loop[0]} = step {loop[1]}")
 
             elif dumpall:
                 print_anyconsts(num_steps)