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

Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aig

This commit is contained in:
Clifford Wolf 2016-12-03 12:37:20 +01:00
parent 8a90e61c1a
commit 37760541bd
1 changed files with 15 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
backends/smt2/smtbmc.py
View File

@ -337,6 +337,11 @@ assert topmod is not None
assert topmod in smt.modinfo assert topmod in smt.modinfo
if cexfile is not None: if cexfile is not None:
if not got_topt:
assume_skipped = 0
skip_steps = 0
num_steps = 0
with open(cexfile, "r") as f: with open(cexfile, "r") as f:
cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])') cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
for entry in f.read().split(): for entry in f.read().split():
@ -368,11 +373,20 @@ if cexfile is not None:
# print("cex@%d: %s" % (step, smtexpr)) # print("cex@%d: %s" % (step, smtexpr))
constr_assumes[step].append((cexfile, smtexpr)) constr_assumes[step].append((cexfile, smtexpr))
if not got_topt:
skip_steps = max(skip_steps, step)
num_steps = max(num_steps, step+1)
if aigprefix is not None: if aigprefix is not None:
input_map = dict() input_map = dict()
init_map = dict() init_map = dict()
latch_map = dict() latch_map = dict()
if not got_topt:
assume_skipped = 0
skip_steps = 0
num_steps = 0
with open(aigprefix + ".aim", "r") as f: with open(aigprefix + ".aim", "r") as f:
for entry in f.read().splitlines(): for entry in f.read().splitlines():
entry = entry.split() entry = entry.split()
@ -473,8 +487,7 @@ if aigprefix is not None:
constr_assumes[step].append((cexfile, smtexpr)) constr_assumes[step].append((cexfile, smtexpr))
if not got_topt: if not got_topt:
skip_steps = step skip_steps = max(skip_steps, step)
assume_skipped = 0
num_steps = max(num_steps, step+1) num_steps = max(num_steps, step+1)
step += 1 step += 1