diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index efab714..e0c8428 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -85,7 +85,7 @@ def run(mode, job, engine_idx, engine): if task_status == "FAIL" and job.opt_aigsmt != "none": 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 " + + ("cd %s; %s -s %s%s --noprogress --append %d -g --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw --aig-noheader 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, diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index b5b20e4..1fd59b8 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -93,7 +93,7 @@ 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 " + + ("cd %s; %s -g -s %s%s --noprogress -g --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw 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, @@ -101,7 +101,7 @@ def run(mode, job, engine_idx, engine): 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 " + + ("cd %s; %s -s %s%s --noprogress --append %d -g --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw 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, diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index ec83c27..b9ea72b 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -128,7 +128,7 @@ def run(mode, job, engine_idx, engine): t_opt = "%d" % job.opt_depth task = SbyTask(job, taskname, job.model(model_name), - "cd %s; %s %s -t %s --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" % + "cd %s; %s %s -t %s --append %d -g --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" % (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name), logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress))