From 363273df5206408d3094a211d5830628f18a9d8e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 30 Jan 2017 11:57:04 +0100 Subject: [PATCH] Refactor engine/mode interfaces --- sbysrc/sby_core.py | 4 +- sbysrc/{sby_bmc.py => sby_engine_abc.py} | 83 +----------------------- sbysrc/sby_engine_smtbmc.py | 76 ++++++++++++++++++++++ sbysrc/sby_mode_bmc.py | 47 ++++++++++++++ 4 files changed, 126 insertions(+), 84 deletions(-) rename sbysrc/{sby_bmc.py => sby_engine_abc.py} (58%) create mode 100644 sbysrc/sby_engine_smtbmc.py create mode 100644 sbysrc/sby_mode_bmc.py diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index ea9ee56..c9956cf 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -329,8 +329,8 @@ class SbyJob: self.copy_src() if self.options["mode"] == "bmc": - import sby_bmc - sby_bmc.run(self) + import sby_mode_bmc + sby_mode_bmc.run(self) else: assert False diff --git a/sbysrc/sby_bmc.py b/sbysrc/sby_engine_abc.py similarity index 58% rename from sbysrc/sby_bmc.py rename to sbysrc/sby_engine_abc.py index cd3ce01..42a8d58 100644 --- a/sbysrc/sby_bmc.py +++ b/sbysrc/sby_engine_abc.py @@ -17,65 +17,9 @@ # import re, os, getopt -from shutil import copyfile from sby_core import SbyTask -def run_smtbmc(job, engine_idx, engine): - smtbmc_opts = [] - nomem_opt = False - syn_opt = False - - opts, args = getopt.getopt(engine[1:], "s:", ["nomem", "syn"]) - assert len(args) == 0 - - for o, a in opts: - if o == "-s": - smtbmc_opts += ["-s", a] - elif o == "--nomem": - nomem_opt = True - elif o == "--syn": - syn_opt = True - else: - assert False - - model_name = "smt2" - if syn_opt: model_name += "_syn" - if nomem_opt: model_name += "_nomem" - - task = SbyTask(job, "engine_%d" % engine_idx, job.model(model_name), - ("cd %s; yosys-smtbmc --noprogress %s -t %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + - "--dump-smtc engine_%d/trace.smtc model/design_smt2.smt2") % - (job.workdir, " ".join(smtbmc_opts), job.opt_depth, engine_idx, engine_idx, engine_idx), - logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w")) - - task_status = None - - def output_callback(line): - nonlocal task_status - - match = re.match(r"^## [0-9: ]+ Status: FAILED", line) - if match: task_status = "FAIL" - - match = re.match(r"^## [0-9: ]+ Status: PASSED", line) - if match: task_status = "PASS" - - def exit_callback(retcode): - assert task_status is not None - - job.status = task_status - job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status)) - job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), job.status)) - - if job.status == "FAIL": - job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) - - job.terminate() - - task.output_callback = output_callback - task.exit_callback = exit_callback - - -def run_abc(job, engine_idx, engine): +def run(mode, job, engine_idx, engine): assert engine == ["abc", "bmc3"] task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), @@ -137,28 +81,3 @@ def run_abc(job, engine_idx, engine): task.output_callback = output_callback task.exit_callback = exit_callback - -def run(job): - job.opt_depth = 20 - - if "depth" in job.options: - job.opt_depth = int(job.options["depth"]) - - for engine_idx in range(len(job.engines)): - engine = job.engines[engine_idx] - assert len(engine) > 0 - - job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) - os.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) - - if engine[0] == "smtbmc": - run_smtbmc(job, engine_idx, engine) - - elif engine[0] == "abc": - run_abc(job, engine_idx, engine) - - else: - assert False - - job.taskloop() - diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py new file mode 100644 index 0000000..8143db1 --- /dev/null +++ b/sbysrc/sby_engine_smtbmc.py @@ -0,0 +1,76 @@ +# +# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# +# Copyright (C) 2016 Clifford Wolf +# +# Permission to use, copy, modify, and/or distribute this software for any +# purpose with or without fee is hereby granted, provided that the above +# copyright notice and this permission notice appear in all copies. +# +# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +# + +import re, os, getopt +from sby_core import SbyTask + +def run(mode, job, engine_idx, engine): + smtbmc_opts = [] + nomem_opt = False + syn_opt = False + + opts, args = getopt.getopt(engine[1:], "s:", ["nomem", "syn"]) + assert len(args) == 0 + + for o, a in opts: + if o == "-s": + smtbmc_opts += ["-s", a] + elif o == "--nomem": + nomem_opt = True + elif o == "--syn": + syn_opt = True + else: + assert False + + model_name = "smt2" + if syn_opt: model_name += "_syn" + if nomem_opt: model_name += "_nomem" + + task = SbyTask(job, "engine_%d" % engine_idx, job.model(model_name), + ("cd %s; yosys-smtbmc --noprogress %s -t %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + + "--dump-smtc engine_%d/trace.smtc model/design_smt2.smt2") % + (job.workdir, " ".join(smtbmc_opts), job.opt_depth, engine_idx, engine_idx, engine_idx), + logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w")) + + task_status = None + + def output_callback(line): + nonlocal task_status + + match = re.match(r"^## [0-9: ]+ Status: FAILED", line) + if match: task_status = "FAIL" + + match = re.match(r"^## [0-9: ]+ Status: PASSED", line) + if match: task_status = "PASS" + + def exit_callback(retcode): + assert task_status is not None + + job.status = task_status + job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status)) + job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), job.status)) + + if job.status == "FAIL": + job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) + + job.terminate() + + task.output_callback = output_callback + task.exit_callback = exit_callback + + diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py new file mode 100644 index 0000000..9a69127 --- /dev/null +++ b/sbysrc/sby_mode_bmc.py @@ -0,0 +1,47 @@ +# +# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows +# +# Copyright (C) 2016 Clifford Wolf +# +# Permission to use, copy, modify, and/or distribute this software for any +# purpose with or without fee is hereby granted, provided that the above +# copyright notice and this permission notice appear in all copies. +# +# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES +# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR +# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES +# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN +# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF +# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. +# + +import re, os, getopt +from sby_core import SbyTask + +def run(job): + job.opt_depth = 20 + + if "depth" in job.options: + job.opt_depth = int(job.options["depth"]) + + for engine_idx in range(len(job.engines)): + engine = job.engines[engine_idx] + assert len(engine) > 0 + + job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) + os.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) + + if engine[0] == "smtbmc": + import sby_engine_smtbmc + sby_engine_smtbmc.run("bmc", job, engine_idx, engine) + + elif engine[0] == "abc": + import sby_engine_abc + sby_engine_abc.run("bmc", job, engine_idx, engine) + + else: + assert False + + job.taskloop() + -- 2.30.2