From bf47da495b44d592615a1e6a7b92d23ab30a48f0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 12 Sep 2018 13:12:24 +0200 Subject: [PATCH] Add "skip" options (smtbmc only) Signed-off-by: Clifford Wolf --- docs/source/reference.rst | 4 ++++ sbysrc/sby_core.py | 9 +++++++++ sbysrc/sby_engine_smtbmc.py | 10 ++++++++-- 3 files changed, 21 insertions(+), 2 deletions(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 9d2871c..5143fd8 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -159,6 +159,10 @@ options are: | | | engine. Other engines ignore this option in ``prove`` | | | | mode. Default: ``20`` | +------------------+------------+---------------------------------------------------------+ +| ``skip`` | ``bmc``, | Skip the specified number of time steps. Only valid | +| | ``cover`` | with smtbmc engine. All other engines are disabled when | +| | | this option is used. Default: None | ++------------------+------------+---------------------------------------------------------+ | ``append`` | ``bmc``, | When generating a counter-example trace, add the | | | ``prove``, | specified number of cycles at the end of the trace. | | | ``cover`` | Default: ``0`` | diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 16462a4..f2792ad 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -497,6 +497,7 @@ class SbyJob: self.handle_int_option("timeout", None) self.handle_str_option("smtc", None) + self.handle_int_option("skip", None) self.handle_str_option("tbtop", None) if self.opt_smtc is not None: @@ -504,6 +505,14 @@ class SbyJob: if engine[0] != "smtbmc": self.error("Option smtc is only valid for smtbmc engine.") + if self.opt_skip is not None: + if self.opt_skip == 0: + self.opt_skip = None + else: + for engine in self.engines: + if engine[0] != "smtbmc": + self.error("Option skip is only valid for smtbmc engine.") + self.copy_src() if self.opt_mode == "bmc": diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index bea1123..ec83c27 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -121,9 +121,15 @@ def run(mode, job, engine_idx, engine): if not progress: smtbmc_opts.append("--noprogress") + + if job.opt_skip is not None: + t_opt = "%d:%d" % (job.opt_skip, job.opt_depth) + else: + t_opt = "%d" % job.opt_depth + task = SbyTask(job, taskname, job.model(model_name), - "cd %s; %s %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), + "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" % + (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)) if mode == "prove_basecase": -- 2.30.2