Add options to set tool paths

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] <jobname>.sby
 
     -b
         backup workdir if it already exists
+
+    --yosys <path_to_executable>
+    --abc <path_to_executable>
+    --smtbmc <path_to_executable>
+    --sprove <path_to_executable>
+        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)

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]

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

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":