From 6878ba0a8250a5aa0f94368fe482a5a987821767 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 10 Dec 2018 02:42:03 +0100 Subject: [PATCH] Improve BTOR cex handling Signed-off-by: Clifford Wolf --- sbysrc/sby_engine_btor.py | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index ec536b6..29bd36b 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -84,6 +84,8 @@ def run(mode, job, engine_idx, engine): assert retcode == 0 assert task_status is not None + if task_status == "PASS": + print("unsat", file=wit_file) wit_file.close() job.update_status(task_status) @@ -96,19 +98,21 @@ def run(mode, job, engine_idx, engine): if produced_cex: if mode == "live": task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), - ("cd %s; %s -g -s %s%s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + - "--dump-smtc engine_%d/trace.smtc --btorwit model/design_btor.btor:engine_%d/trace.wit model/design_smt2.smt2") % - (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, - engine_idx, engine_idx, engine_idx, engine_idx), + ("cd %s; btorsim --states model/design_btor.btor engine_%d/trace.wit > engine_%d/simtrace.wit && " + + "%s -g -s %s%s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + + "--dump-smtc engine_%d/trace.smtc --btorwit engine_%d/simtrace.wit model/design_smt2.smt2") % + (job.workdir, engine_idx, engine_idx, job.exe_paths["smtbmc"], job.opt_aigsmt, + "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, + engine_idx, engine_idx, engine_idx, engine_idx), logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) else: task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), - ("cd %s; %s -s %s%s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + - "--dump-smtc engine_%d/trace.smtc --btorwit model/design_btor.btor:engine_%d/trace.wit model/design_smt2.smt2") % - (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, - job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx), + ("cd %s; btorsim --states model/design_btor.btor engine_%d/trace.wit > engine_%d/simtrace.wit && " + + "%s -s %s%s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + + "--dump-smtc engine_%d/trace.smtc --btorwit engine_%d/simtrace.wit model/design_smt2.smt2") % + (job.workdir, engine_idx, engine_idx, job.exe_paths["smtbmc"], job.opt_aigsmt, + "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, + job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx), logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) task2_status = None -- 2.30.2