mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-12 16:28:17 +00:00
Make --presat and --unroll the default for smtbmc
This commit is contained in:
parent
20b8b8fe9f
commit
82f394260a
|
@ -22,11 +22,13 @@ from sby_core import SbyTask
|
||||||
def run(mode, job, engine_idx, engine):
|
def run(mode, job, engine_idx, engine):
|
||||||
smtbmc_opts = []
|
smtbmc_opts = []
|
||||||
nomem_opt = False
|
nomem_opt = False
|
||||||
|
presat_opt = True
|
||||||
|
unroll_opt = True
|
||||||
syn_opt = False
|
syn_opt = False
|
||||||
stbv_opt = False
|
stbv_opt = False
|
||||||
dumpsmt2 = False
|
dumpsmt2 = False
|
||||||
|
|
||||||
opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "presat", "unroll", "dumpsmt2"])
|
opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "presat", "nopresat", "unroll", "nounroll", "dumpsmt2"])
|
||||||
|
|
||||||
for o, a in opts:
|
for o, a in opts:
|
||||||
if o == "--nomem":
|
if o == "--nomem":
|
||||||
|
@ -36,14 +38,24 @@ def run(mode, job, engine_idx, engine):
|
||||||
elif o == "--stbv":
|
elif o == "--stbv":
|
||||||
stbv_opt = True
|
stbv_opt = True
|
||||||
elif o == "--presat":
|
elif o == "--presat":
|
||||||
smtbmc_opts += ["--presat"]
|
presat_opt = True
|
||||||
|
elif o == "--nopresat":
|
||||||
|
presat_opt = False
|
||||||
elif o == "--unroll":
|
elif o == "--unroll":
|
||||||
smtbmc_opts += ["--unroll"]
|
unroll_opt = True
|
||||||
|
elif o == "--nounroll":
|
||||||
|
unroll_opt = False
|
||||||
elif o == "--dumpsmt2":
|
elif o == "--dumpsmt2":
|
||||||
dumpsmt2 = True
|
dumpsmt2 = True
|
||||||
else:
|
else:
|
||||||
assert False
|
assert False
|
||||||
|
|
||||||
|
if presat_opt:
|
||||||
|
smtbmc_opts += ["--presat"]
|
||||||
|
|
||||||
|
if unroll_opt:
|
||||||
|
smtbmc_opts += ["--unroll"]
|
||||||
|
|
||||||
for i, a in enumerate(args):
|
for i, a in enumerate(args):
|
||||||
smtbmc_opts += ["-s" if i == 0 else "-S", a]
|
smtbmc_opts += ["-s" if i == 0 else "-S", a]
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue