From 3e816e992224612ace7d43171e8c1993b7e8238d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Sun, 9 Oct 2022 18:24:43 +0200 Subject: [PATCH 1/5] experimental temporal induction counterexample loop detection --- backends/smt2/smtbmc.py | 44 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 5f05287de..4997833f4 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 +find_loops = False so = SmtOpts() @@ -175,6 +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 + """ + so.helpmsg()) sys.exit(1) @@ -183,7 +187,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", "find-loops"]) except: usage() @@ -264,6 +268,8 @@ for o, a in opts: keep_going = True elif o == "--check-witness": check_witness = True + elif o == "--find-loops": + find_loops = True elif so.handle(o, a): pass else: @@ -969,6 +975,38 @@ 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") + + 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) + + mem_trace_data = collect_mem_trace_data(steps_start, steps_stop) + + 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)) + 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): if ('A' <= c <= 'Z'): return True if ('a' <= c <= 'z'): return True @@ -1596,6 +1634,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 loop: + print_msg(f"Loop detected, increasing induction depth will not help. Cycle {loop[0]} = cycle {loop[1]}") elif dumpall: print_anyconsts(num_steps) 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 2/5] 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) From 8d4000a9b75dd636e9609b9e6a05d7ae3d7a9dee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Tue, 11 Oct 2022 19:52:44 +0200 Subject: [PATCH 3/5] include memory in state --- backends/smt2/smtbmc.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index fd54622f2..c25f529b9 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -991,8 +991,7 @@ def detect_state_loop(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, [])] - ) + 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]) From 083ca6ab066d01aa33156860bb4e29efe547f834 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Tue, 18 Oct 2022 22:58:54 +0200 Subject: [PATCH 4/5] bugfix --- backends/smt2/smtbmc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index c25f529b9..cc108d52b 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -993,7 +993,7 @@ def detect_state_loop(steps_start, steps_stop): [(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): + if state in states: return (i, states[state]) else: states[state] = i From 2ba435b6bc0a5f0f831c331abdf8d58e0fdae132 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Emil=20Ji=C5=99=C3=AD=20Tywoniak?= Date: Thu, 20 Oct 2022 19:31:16 +0200 Subject: [PATCH 5/5] bugfix for mathsat counterexample vcd dump --- backends/smt2/smtio.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 9af454cca..5cd1a74fb 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -917,7 +917,7 @@ class SmtIo: if len(expr_list) == 0: return [] self.write("(get-value (%s))" % " ".join(expr_list)) - return [n[1] for n in self.parse(self.read())] + return [n[1] for n in self.parse(self.read()) if n] def get_path(self, mod, path): assert mod in self.modinfo