From: Clifford Wolf Date: Sat, 8 Dec 2018 04:23:04 +0000 (+0100) Subject: Add btor engine X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4c485766e27d7d538fc3b62cadbdff30fffdb7af;p=SymbiYosys.git Add btor engine Signed-off-by: Clifford Wolf --- diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 435119d..8bf19cf 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -59,13 +59,14 @@ sby [options] [.sby [tasknames]] --suprove --aigbmc --avy + --btormc configure which executable to use for the respective tool """) sys.exit(1) try: opts, args = getopt.getopt(sys.argv[1:], "d:btfT:E", ["yosys=", - "abc=", "smtbmc=", "suprove=", "aigbmc=", "avy="]) + "abc=", "smtbmc=", "suprove=", "aigbmc=", "avy=", "btormc="]) except: usage() @@ -94,6 +95,8 @@ for o, a in opts: exe_paths["aigbmc"] = a elif o == "--avy": exe_paths["avy"] = a + elif o == "--btormc": + exe_paths["btormc"] = a else: usage() diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index fa80526..2eea8ed 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -153,6 +153,7 @@ class SbyJob: "suprove": "suprove", "aigbmc": "aigbmc", "avy": "avy", + "btormc": "btormc", } self.tasks_running = [] @@ -333,6 +334,24 @@ class SbyJob: return [task] + if re.match(r"^btor(_syn)?(_nomem)?$", model_name): + with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f: + print("# running in %s/model/" % (self.workdir), file=f) + print("read_ilang design%s.il" % ("_nomem" if "_nomem" in model_name else ""), file=f) + if "_syn" in model_name: + print("techmap", file=f) + print("opt -fast", file=f) + print("abc", file=f) + print("opt_clean", file=f) + print("stat", file=f) + print("write_btor design_%s.btor" % model_name, file=f) + + task = SbyTask(self, model_name, self.model("nomem" if "_nomem" in model_name else "base"), + "cd %s/model; %s -ql design_%s.log design_%s.ys" % (self.workdir, self.exe_paths["yosys"], model_name, model_name)) + task.checkretcode = True + + return [task] + if model_name == "aig": with open("%s/model/design_aiger.ys" % (self.workdir), "w") as f: print("# running in %s/model/" % (self.workdir), file=f) diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py new file mode 100644 index 0000000..8b9a9cc --- /dev/null +++ b/sbysrc/sby_engine_btor.py @@ -0,0 +1,137 @@ +# +# 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): + opts, solver_args = getopt.getopt(engine[1:], "", []) + + if len(solver_args) == 0: + job.error("Missing solver command.") + + for o, a in opts: + job.error("Unexpected BTOR engine options.") + + if solver_args[0] == "btormc": + solver_cmd = job.exe_paths["btormc"] + " --stop-first -kmax %d" % job.opt_depth + if job.opt_skip is not None: + solver_cmd += " -kmin %d" % job.opt_skip + solver_cmd += " ".join([""] + solver_args[1:]) + + else: + job.error("Invalid solver command %s." % solver_args[0]) + + task = SbyTask(job, "engine_%d" % engine_idx, job.model("btor"), + "cd %s; %s model/design_btor.btor" % (job.workdir, solver_cmd), + logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w")) + + task_status = None + produced_cex = False + end_of_cex = False + aiw_file = open("%s/engine_%d/trace.aiw" % (job.workdir, engine_idx), "w") + + def output_callback(line): + nonlocal task_status + nonlocal produced_cex + nonlocal end_of_cex + + if task_status is not None: + if not end_of_cex and not produced_cex and line.isdigit(): + produced_cex = True + if not end_of_cex: + print(line, file=aiw_file) + if line == ".": + end_of_cex = True + return None + + if line.startswith("u"): + return "No CEX up to depth %d." % (int(line[1:])-1) + + if line in ["0", "1", "2"]: + print(line, file=aiw_file) + if line == "0": task_status = "PASS" + if line == "1": task_status = "FAIL" + if line == "2": task_status = "UNKNOWN" + + return None + + def exit_callback(retcode): + if solver_args[0] not in ["avy"]: + assert retcode == 0 + assert task_status is not None + + aiw_file.close() + + job.update_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), task_status)) + + job.terminate() + + if task_status == "FAIL" and job.opt_aigsmt != "none": + 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 " + + "--dump-smtc engine_%d/trace.smtc --aig model/design_btor.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, + engine_idx, engine_idx, engine_idx, engine_idx), + 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 " + + "--dump-smtc engine_%d/trace.smtc --aig model/design_btor.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, + job.opt_append, 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" + + return line + + def exit_callback2(line): + assert task2_status is not None + if mode == "live": + assert task2_status == "PASS" + else: + assert task2_status == "FAIL" + + if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)): + job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) + + task2.output_callback = output_callback2 + task2.exit_callback = exit_callback2 + + else: + job.log("engine_%d: Engine did not produce a counter example." % engine_idx) + + task.output_callback = output_callback + task.exit_callback = exit_callback + diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index 5e6236d..c3c55ea 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -39,6 +39,10 @@ def run(job): import sby_engine_abc sby_engine_abc.run("bmc", job, engine_idx, engine) + elif engine[0] == "btor": + import sby_engine_btor + sby_engine_btor.run("bmc", job, engine_idx, engine) + else: job.error("Invalid engine '%s' for bmc mode." % engine[0])