From 7085657687f19392bc119734d619a4f585660b2e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 9 Feb 2017 14:09:14 +0100 Subject: [PATCH] Add options to set tool paths --- sbysrc/sby.py | 22 +++++++++++++++++++++- sbysrc/sby_core.py | 13 ++++++++++--- sbysrc/sby_engine_abc.py | 16 ++++++---------- sbysrc/sby_engine_smtbmc.py | 4 ++-- 4 files changed, 39 insertions(+), 16 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 14667d6..94ec952 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -25,6 +25,7 @@ sbyfile = None workdir = None opt_force = False opt_backup = False +exe_paths = dict() def usage(): print(""" @@ -38,11 +39,18 @@ sby [options] .sby -b backup workdir if it already exists + + --yosys + --abc + --smtbmc + --sprove + configure which executable to use for the respective tool """) sys.exit(1) try: - opts, args = getopt.getopt(sys.argv[1:], "d:bf", []) + opts, args = getopt.getopt(sys.argv[1:], "d:bf", ["yosys=", + "abc=", "smtbmc=", "sprove="]) except: usage() @@ -53,6 +61,14 @@ for o, a in opts: opt_force = True elif o == "-b": opt_backup = True + elif o == "--yosys": + exe_paths["yosys"] = a + elif o == "--abc": + exe_paths["abc"] = a + elif o == "--smtbmc": + exe_paths["smtbmc"] = a + elif o == "--sprove": + exe_paths["sprove"] = a else: usage() @@ -82,6 +98,10 @@ if opt_force: shutil.rmtree(workdir, ignore_errors=True) job = SbyJob(sbyfile, workdir, early_logmsgs) + +for k, v in exe_paths.items(): + job.exe_paths[k] = v + job.run() sys.exit(job.retcode) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 705d4e0..d53d7d6 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -132,6 +132,13 @@ class SbyJob: self.workdir = workdir self.status = "UNKNOWN" + self.exe_paths = { + "yosys": "yosys", + "abc": "yosys-abc", + "smtbmc": "yosys-smtbmc", + "sprove": "super_prove", + } + self.tasks_running = [] self.tasks_all = [] @@ -298,7 +305,7 @@ class SbyJob: print("write_ilang ../model/design.il", file=f) task = SbyTask(self, "script", [], - "cd %s/src; yosys -ql ../model/design.log ../model/design.ys" % (self.workdir)) + "cd %s/src; %s -ql ../model/design.log ../model/design.ys" % (self.workdir, self.exe_paths["yosys"])) task.checkretcode = True return [task] @@ -319,7 +326,7 @@ class SbyJob: print("write_smt2 -wires design_%s.smt2" % model_name, file=f) task = SbyTask(self, model_name, self.model("ilang"), - "cd %s/model; yosys -ql design_%s.log design_%s.ys" % (self.workdir, model_name, model_name)) + "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] @@ -342,7 +349,7 @@ class SbyJob: print("write_aiger -zinit -map design_aiger.aim design_aiger.aig", file=f) task = SbyTask(self, "aig", self.model("ilang"), - "cd %s/model; yosys -ql design_aiger.log design_aiger.ys" % (self.workdir)) + "cd %s/model; %s -ql design_aiger.log design_aiger.ys" % (self.workdir, self.exe_paths["yosys"])) task.checkretcode = True return [task] diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 9aa0d48..4230620 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -29,25 +29,21 @@ def run(mode, job, engine_idx, engine): if abc_command[0] == "bmc3": assert mode == "bmc" assert len(abc_command) == 1 - abc_script = "bmc3 -F %d -v" % job.opt_depth + abc_command[0] += " -F %d -v" % job.opt_depth elif abc_command[0] == "sim3": assert mode == "bmc" - abc_script = "sim3 -F %d -v" % job.opt_depth + abc_command[0] += " -F %d -v" % job.opt_depth elif abc_command[0] == "pdr": assert mode == "prove" - abc_script = "pdr" else: assert False - if len(abc_command) > 1: - abc_script += " " + " ".join(abc_command[1:]) - task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), - ("cd %s; yosys-abc -c 'read_aiger model/design_aiger.aig; fold; strash; %s; " + - "write_cex -a engine_%d/trace.aiw'") % (job.workdir, abc_script, engine_idx), + ("cd %s; %s -c 'read_aiger model/design_aiger.aig; fold; strash; %s; write_cex -a engine_%d/trace.aiw'") % + (job.workdir, job.exe_paths["abc"], " ".join(abc_command), engine_idx), logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w")) task.noprintregex = re.compile(r"^\.+$") @@ -83,9 +79,9 @@ def run(mode, job, engine_idx, engine): if task_status == "FAIL": task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), - ("cd %s; yosys-smtbmc --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + + ("cd %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_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") % - (job.workdir, engine_idx, engine_idx, engine_idx, engine_idx), + (job.workdir, job.exe_paths["smtbmc"], engine_idx, engine_idx, engine_idx, engine_idx), logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) task2_status = None diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 0ac29fc..cb07111 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -65,8 +65,8 @@ def run(mode, job, engine_idx, engine): trace_prefix += "%" task = SbyTask(job, taskname, job.model(model_name), - ("cd %s; yosys-smtbmc --noprogress %s -t %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_smt2.smt2") % - (job.workdir, " ".join(smtbmc_opts), job.opt_depth, trace_prefix, trace_prefix, trace_prefix), + ("cd %s; %s --noprogress %s -t %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_smt2.smt2") % + (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), job.opt_depth, trace_prefix, trace_prefix, trace_prefix), logfile=open(logfile_prefix + ".txt", "w")) if mode == "prove_basecase": -- 2.30.2