mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-06 14:24:08 +00:00
Code Activity

smtbmc: Allow using --keep-going in cover mode

Browse source 
See YosysHQ/yosys#3816 for the smtbmc change that made --keep-going do
something in cover mode
This commit is contained in:
Jannis Harder 2023-06-23 10:31:17 +02:00
parent c027aea3db
commit 28c053bd94
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
sbysrc/sby_engine_smtbmc.py
View file

@ -69,8 +69,6 @@ def run(mode, task, engine_idx, engine):
task.error("smtbmc options --basecase and --induction are exclusive.") task.error("smtbmc options --basecase and --induction are exclusive.")
induction_only = True induction_only = True
elif o == "--keep-going": elif o == "--keep-going":
if mode not in ("bmc", "prove", "prove_basecase", "prove_induction"):
task.error("smtbmc option --keep-going is only supported in bmc and prove mode.")
keep_going = True keep_going = True
elif o == "--seed": elif o == "--seed":
random_seed = a random_seed = a
@ -134,7 +132,8 @@ def run(mode, task, engine_idx, engine):
if keep_going and mode != "prove_induction": if keep_going and mode != "prove_induction":
smtbmc_opts.append("--keep-going") smtbmc_opts.append("--keep-going")
trace_prefix += "%" if mode != "cover":
trace_prefix += "%"
if dumpsmt2: if dumpsmt2:
smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"] smtbmc_opts += ["--dump-smt2", trace_prefix.replace("%", "") + ".smt2"]