From 0dbebea939ec52dfa2a0d522adfede123405a81c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Tue, 11 Oct 2022 19:48:16 +0200 Subject: [PATCH] include memory in state --- backends/smt2/smtbmc.py | 48 ++++++++++++++++++----------------------- 1 file changed, 21 insertions(+), 27 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 4997833f4..fd54622f2 100644 --- a/backends/smt2/smtbmc.py +++ b/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)