mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-09-04 18:47:43 +00:00
Code Activity

Add --anybase option to smtbmc engine

Browse source 
This uses the smtbmc -g flag to generate an arbitrary trace for the
basecase in prove mode, instead of one starting with the initial
conditions. This behaves similarly to the basecase assertions in yosys'
equiv_induct.
This commit is contained in:
George Rennie 2021-11-16 15:16:32 +00:00
parent 15278f1346
commit 79634d5016
1 changed files with 23 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

30
sbysrc/sby_engine_smtbmc.py
View file

@ -29,12 +29,14 @@ def run(mode, job, engine_idx, engine):
stdt_opt = False stdt_opt = False
dumpsmt2 = False dumpsmt2 = False
progress = False progress = False
anybase = False
basecase_only = False basecase_only = False
induction_only = False induction_only = False
random_seed = None random_seed = None
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", "basecase", "induction", "seed="]) "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "anybase",
"basecase", "induction", "seed="])
for o, a in opts: for o, a in opts:
if o == "--nomem": if o == "--nomem":
@ -57,6 +59,8 @@ def run(mode, job, engine_idx, engine):
dumpsmt2 = True dumpsmt2 = True
elif o == "--progress": elif o == "--progress":
progress = True progress = True
elif o == "--anybase":
anybase = True
elif o == "--basecase": elif o == "--basecase":
if induction_only: if induction_only:
job.error("smtbmc options --basecase and --induction are exclusive.") job.error("smtbmc options --basecase and --induction are exclusive.")
@ -114,6 +118,8 @@ def run(mode, job, engine_idx, engine):
if mode == "prove_basecase": if mode == "prove_basecase":
taskname += ".basecase" taskname += ".basecase"
logfile_prefix += "_basecase" logfile_prefix += "_basecase"
if anybase:
smtbmc_opts.append("-g")
if mode == "prove_induction": if mode == "prove_induction":
taskname += ".induction" taskname += ".induction"
@ -218,14 +224,24 @@ def run(mode, job, engine_idx, engine):
for task in job.basecase_tasks: for task in job.basecase_tasks:
task.terminate() task.terminate()
if task_status == "PASS": if not anybase:
job.basecase_pass = True if task_status == "PASS":
job.basecase_pass = True
else:
job.update_status(task_status)
if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"):
job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd")
job.terminate()
else: else:
job.update_status(task_status) if task_status == "PASS":
if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"): job.basecase_pass = True
job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd") if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"):
job.terminate() job.summary.append(f"basecase trace: {job.workdir}/engine_{engine_idx}/trace.vcd")
else:
job.update_status(task_status)
job.terminate()
elif mode == "prove_induction": elif mode == "prove_induction":
for task in job.induction_tasks: for task in job.induction_tasks: