diff options
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 37 |
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) |