diff options
author | Emil J <emil.tywoniak@gmail.com> | 2022-10-19 12:20:12 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-10-19 12:20:12 +0200 |
commit | 8859d801c83b6d67279bb907837bb7b08d2f338e (patch) | |
tree | 06602fe3b308c3b36a9d19efdd08399f477ebab1 /backends | |
parent | f4ede15d6857c02576a32f94043af866fde607aa (diff) | |
download | yosys-8859d801c83b6d67279bb907837bb7b08d2f338e.tar.gz yosys-8859d801c83b6d67279bb907837bb7b08d2f338e.tar.bz2 yosys-8859d801c83b6d67279bb907837bb7b08d2f338e.zip |
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.
Diffstat (limited to 'backends')
-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) |