aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorEmil J <emil.tywoniak@gmail.com>2022-10-19 12:20:12 +0200
committerGitHub <noreply@github.com>2022-10-19 12:20:12 +0200
commit8859d801c83b6d67279bb907837bb7b08d2f338e (patch)
tree06602fe3b308c3b36a9d19efdd08399f477ebab1 /backends
parentf4ede15d6857c02576a32f94043af866fde607aa (diff)
downloadyosys-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.py37
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)