From: Clifford Wolf Date: Mon, 30 Jan 2017 10:57:04 +0000 (+0100) Subject: Refactor engine/mode interfaces X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=363273df5206408d3094a211d5830628f18a9d8e;p=SymbiYosys.git Refactor engine/mode interfaces --- diff --git a/sbysrc/sby_bmc.py b/sbysrc/sby_bmc.py deleted file mode 100644 index cd3ce01..0000000 --- a/sbysrc/sby_bmc.py +++ /dev/null @@ -1,164 +0,0 @@ -# -# 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 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): - assert engine == ["abc", "bmc3"] - - task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), - ("cd %s; yosys-abc -c 'read_aiger model/design_aiger.aig; fold; strash; bmc3 -F %d -v; " + - "undc -c; write_cex -a engine_%d/trace.aiw'") % (job.workdir, job.opt_depth, 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"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line) - if match: task_status = "FAIL" - - match = re.match(r"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line) - if match: task_status = "PASS" - - match = re.match(r"^No output asserted in [0-9]+ frames.", line) - if match: task_status = "PASS" - - def exit_callback(retcode): - assert retcode == 0 - 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)) - - job.terminate() - - if job.status == "FAIL": - task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), - ("cd %s; yosys-smtbmc --noprogress -t %d --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.opt_depth, engine_idx, engine_idx, engine_idx, engine_idx), - logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) - - task2_status = None - - def output_callback2(line): - nonlocal task2_status - - match = re.match(r"^## [0-9: ]+ Status: FAILED", line) - if match: task2_status = "FAIL" - - match = re.match(r"^## [0-9: ]+ Status: PASSED", line) - if match: task2_status = "PASS" - - def exit_callback2(line): - assert task2_status is not None - assert task2_status == "FAIL" - - job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) - - task2.output_callback = output_callback2 - task2.exit_callback = exit_callback2 - - 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_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_engine_abc.py b/sbysrc/sby_engine_abc.py new file mode 100644 index 0000000..42a8d58 --- /dev/null +++ b/sbysrc/sby_engine_abc.py @@ -0,0 +1,83 @@ +# +# 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): + assert engine == ["abc", "bmc3"] + + task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), + ("cd %s; yosys-abc -c 'read_aiger model/design_aiger.aig; fold; strash; bmc3 -F %d -v; " + + "undc -c; write_cex -a engine_%d/trace.aiw'") % (job.workdir, job.opt_depth, 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"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line) + if match: task_status = "FAIL" + + match = re.match(r"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line) + if match: task_status = "PASS" + + match = re.match(r"^No output asserted in [0-9]+ frames.", line) + if match: task_status = "PASS" + + def exit_callback(retcode): + assert retcode == 0 + 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)) + + job.terminate() + + if job.status == "FAIL": + task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), + ("cd %s; yosys-smtbmc --noprogress -t %d --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.opt_depth, engine_idx, engine_idx, engine_idx, engine_idx), + logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) + + task2_status = None + + def output_callback2(line): + nonlocal task2_status + + match = re.match(r"^## [0-9: ]+ Status: FAILED", line) + if match: task2_status = "FAIL" + + match = re.match(r"^## [0-9: ]+ Status: PASSED", line) + if match: task2_status = "PASS" + + def exit_callback2(line): + assert task2_status is not None + assert task2_status == "FAIL" + + job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) + + task2.output_callback = output_callback2 + task2.exit_callback = exit_callback2 + + task.output_callback = output_callback + task.exit_callback = exit_callback + 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() +