riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

yosys-smtbmc: added -i support smtc files

This commit is contained in:
Clifford Wolf 2016-09-18 00:48:36 +02:00
parent d39db41df8
commit 7bc88e8101
1 changed files with 19 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
backends/smt2/smtbmc.py
View File

@ -136,11 +136,6 @@ if len(args) != 1:
usage() usage()
if tempind and len(inconstr) != 0:
print("Error: options -i and --smtc are exclusive.")
sys.exit(1)
constr_final_start = None constr_final_start = None
constr_asserts = defaultdict(list) constr_asserts = defaultdict(list)
constr_assumes = defaultdict(list) constr_assumes = defaultdict(list)
@ -163,7 +158,8 @@ for fn in inconstr:
if tokens[0] == "initial": if tokens[0] == "initial":
current_states = set() current_states = set()
current_states.add(0) if not tempind:
current_states.add(0)
continue continue
if tokens[0] == "final": if tokens[0] == "final":
@ -182,20 +178,21 @@ for fn in inconstr:
if tokens[0] == "state": if tokens[0] == "state":
current_states = set() current_states = set()
for token in tokens[1:]: if not tempind:
tok = token.split(":") for token in tokens[1:]:
if len(tok) == 1: tok = token.split(":")
current_states.add(int(token)) if len(tok) == 1:
elif len(tok) == 2: current_states.add(int(token))
lower = int(tok[0]) elif len(tok) == 2:
if tok[1] == "*": lower = int(tok[0])
upper = num_steps if tok[1] == "*":
upper = num_steps
else:
upper = int(tok[1])
for i in range(lower, upper+1):
current_states.add(i)
else: else:
upper = int(tok[1]) assert 0
for i in range(lower, upper+1):
current_states.add(i)
else:
assert 0
continue continue
if tokens[0] == "always": if tokens[0] == "always":
@ -522,13 +519,15 @@ if tempind:
smt.write("(assert (|%s_u| s%d))" % (topmod, step)) smt.write("(assert (|%s_u| s%d))" % (topmod, step))
smt.write("(assert (|%s_h| s%d))" % (topmod, step)) smt.write("(assert (|%s_h| s%d))" % (topmod, step))
smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
if step == num_steps: if step == num_steps:
smt.write("(assert (not (|%s_a| s%d)))" % (topmod, step)) smt.write("(assert (not (and (|%s_a| s%d) %s)))" % (topmod, step, get_constr_expr(constr_asserts, step)))
else: else:
smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step, step+1)) smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step, step+1))
smt.write("(assert (|%s_a| s%d))" % (topmod, step)) smt.write("(assert (|%s_a| s%d))" % (topmod, step))
smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
if step > num_steps-skip_steps: if step > num_steps-skip_steps:
print_msg("Skipping induction in step %d.." % (step)) print_msg("Skipping induction in step %d.." % (step))