mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

Add "smtbmc --basecase/--induction"

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-07 22:23:50 +01:00
parent 47729cd61c
commit ec38b0b841
1 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
sbysrc/sby_engine_smtbmc.py
View file

@ -29,9 +29,11 @@ def run(mode, job, engine_idx, engine):
stdt_opt = False stdt_opt = False
dumpsmt2 = False dumpsmt2 = False
progress = False progress = False
basecase_only = False
induction_only = False
opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat", opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat",
"nopresat", "unroll", "nounroll", "dumpsmt2", "progress"]) "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction"])
for o, a in opts: for o, a in opts:
if o == "--nomem": if o == "--nomem":
@ -54,6 +56,12 @@ def run(mode, job, engine_idx, engine):
dumpsmt2 = True dumpsmt2 = True
elif o == "--progress": elif o == "--progress":
progress = True progress = True
elif o == "--basecase":
assert not induction_only
basecase_only = True
elif o == "--induction":
assert not basecase_only
induction_only = True
else: else:
assert False assert False
@ -81,8 +89,10 @@ def run(mode, job, engine_idx, engine):
if stdt_opt: model_name += "_stdt" if stdt_opt: model_name += "_stdt"
if mode == "prove": if mode == "prove":
run("prove_basecase", job, engine_idx, engine) if not induction_only:
run("prove_induction", job, engine_idx, engine) run("prove_basecase", job, engine_idx, engine)
if not basecase_only:
run("prove_induction", job, engine_idx, engine)
return return
taskname = "engine_%d" % engine_idx taskname = "engine_%d" % engine_idx