mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-07-19 02:42:03 +00:00
Code Activity

smtbmc: Set step range for --yw and dont skip steps for --check-witness

Browse source
This commit is contained in:
Jannis Harder 2022-08-08 15:33:47 +02:00
parent 927af914f1
commit 66f761a8c5
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
backends/smt2/smtbmc.py
View file

@ -482,6 +482,7 @@ if cexfile is not None:
constr_assumes[step].append((cexfile, smtexpr)) constr_assumes[step].append((cexfile, smtexpr))
if not got_topt: if not got_topt:
if not check_witness:
skip_steps = max(skip_steps, step) skip_steps = max(skip_steps, step)
num_steps = max(num_steps, step+1) num_steps = max(num_steps, step+1)
@ -615,6 +616,7 @@ if aimfile is not None:
constr_assumes[step].append((cexfile, smtexpr)) constr_assumes[step].append((cexfile, smtexpr))
if not got_topt: if not got_topt:
if not check_witness:
skip_steps = max(skip_steps, step) skip_steps = max(skip_steps, step)
# some solvers optimize the properties so that they fail one cycle early, # some solvers optimize the properties so that they fail one cycle early,
# thus we check the properties in the cycle the aiger witness ends, and # thus we check the properties in the cycle the aiger witness ends, and
@ -623,6 +625,11 @@ if aimfile is not None:
step += 1 step += 1
if inywfile is not None: if inywfile is not None:
if not got_topt:
assume_skipped = 0
skip_steps = 0
num_steps = 0
with open(inywfile, "r") as f: with open(inywfile, "r") as f:
inyw = ReadWitness(f) inyw = ReadWitness(f)
@ -717,6 +724,11 @@ if inywfile is not None:
smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
constr_assumes[t].append((inywfile, smt_constr)) constr_assumes[t].append((inywfile, smt_constr))
if not got_topt:
if not check_witness:
skip_steps = max(skip_steps, t)
num_steps = max(num_steps, t+1)
if btorwitfile is not None: if btorwitfile is not None:
with open(btorwitfile, "r") as f: with open(btorwitfile, "r") as f:
step = None step = None