From 78efd64985a2979edc42ef0ccde98634fbb45a0b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 23 Oct 2017 02:17:39 +0200 Subject: [PATCH] Add "smtbmc --dumpsmt2" --- sbysrc/sby_engine_smtbmc.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index cc44f28..3731dc5 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -24,8 +24,9 @@ def run(mode, job, engine_idx, engine): nomem_opt = False syn_opt = False stbv_opt = False + dumpsmt2 = False - opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "presat", "unroll"]) + opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "presat", "unroll", "dumpsmt2"]) for o, a in opts: if o == "--nomem": @@ -38,6 +39,8 @@ def run(mode, job, engine_idx, engine): smtbmc_opts += ["--presat"] elif o == "--unroll": smtbmc_opts += ["--unroll"] + elif o == "--dumpsmt2": + dumpsmt2 = True else: assert False @@ -78,6 +81,9 @@ def run(mode, job, engine_idx, engine): smtbmc_opts.append("-c") trace_prefix += "%" + if dumpsmt2: + smtbmc_opts += ["--dump-smt2", trace_prefix + ".smt2"] + task = SbyTask(job, taskname, job.model(model_name), "cd %s; %s --noprogress %s -t %d --append %d --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), job.opt_depth, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name), -- 2.30.2