mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Handle "always 1" like "always -1" in .smtc files

Browse source
This commit is contained in:
Clifford Wolf 2017-01-02 20:02:52 +01:00
parent f0df7dd796
commit 81bb952e5d
1 changed files with 5 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
backends/smt2/smtbmc.py
View file

@ -201,10 +201,9 @@ for fn in inconstr:
current_states = set(["final-%d" % i for i in range(0, num_steps+1)]) current_states = set(["final-%d" % i for i in range(0, num_steps+1)])
constr_final_start = 0 constr_final_start = 0
elif len(tokens) == 2: elif len(tokens) == 2:
i = int(tokens[1]) arg = abs(int(tokens[1]))
assert i < 0 current_states = set(["final-%d" % i for i in range(arg, num_steps+1)])
current_states = set(["final-%d" % i for i in range(-i, num_steps+1)]) constr_final_start = arg if constr_final_start is None else min(constr_final_start, arg)
constr_final_start = -i if constr_final_start is None else min(constr_final_start, -i)
else: else:
assert False assert False
continue continue
@ -232,9 +231,8 @@ for fn in inconstr:
if len(tokens) == 1: if len(tokens) == 1:
current_states = set(range(0, num_steps+1)) current_states = set(range(0, num_steps+1))
elif len(tokens) == 2: elif len(tokens) == 2:
i = int(tokens[1]) arg = abs(int(tokens[1]))
assert i < 0 current_states = set(range(arg, num_steps+1))
current_states = set(range(-i, num_steps+1))
else: else:
assert False assert False
continue continue