def early_log(workdir, msg):
tm = localtime()
- early_logmsgs.append("SBY %2d:%02d:%02d [%s] %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg))
+ early_logmsgs.append("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg))
print(early_logmsgs[-1])
if len(task_tags_all) and not found_task_tag:
tokens = line.split()
if len(tokens) > 0 and tokens[0][0] == line[0] and tokens[0].endswith(":"):
- print("ERROR: Invalid task specifier \"%s\"." % tokens[0], file=sys.stderr)
+ print("ERROR: Invalid task specifier \"{}\".".format(tokens[0]), file=sys.stderr)
sys.exit(1)
if task_skip_line or task_skip_block:
continue
filename = line.split()[-1]
file_set.add(process_filename(filename))
-
+
if len(tasknames):
for taskname in tasknames:
find_files(taskname)
if my_workdir is not None:
if opt_backup:
backup_idx = 0
- while os.path.exists("%s.bak%03d" % (my_workdir, backup_idx)):
+ while os.path.exists("{}.bak{:03d}".format(my_workdir, backup_idx)):
backup_idx += 1
- early_log(my_workdir, "Moving directory '%s' to '%s'." % (my_workdir, "%s.bak%03d" % (my_workdir, backup_idx)))
- shutil.move(my_workdir, "%s.bak%03d" % (my_workdir, backup_idx))
+ early_log(my_workdir, "Moving directory '{}' to '{}'.".format(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx)))
+ shutil.move(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx))
if opt_force and not reusedir:
- early_log(my_workdir, "Removing directory '%s'." % (my_workdir))
+ early_log(my_workdir, "Removing directory '{}'.".format(my_workdir))
if sbyfile:
shutil.rmtree(my_workdir, ignore_errors=True)
if reusedir:
pass
elif os.path.isdir(my_workdir):
- print("ERROR: Directory '%s' already exists." % (my_workdir))
+ print("ERROR: Directory '{}' already exists.".format(my_workdir))
sys.exit(1)
else:
os.makedirs(my_workdir)
pass
if my_opt_tmpdir:
- job.log("Removing directory '%s'." % (my_workdir))
+ job.log("Removing directory '{}'.".format(my_workdir))
shutil.rmtree(my_workdir, ignore_errors=True)
if setupmode:
- job.log("SETUP COMPLETE (rc=%d)" % (job.retcode))
+ job.log("SETUP COMPLETE (rc={})".format(job.retcode))
else:
- job.log("DONE (%s, rc=%d)" % (job.status, job.retcode))
+ job.log("DONE ({}, rc={})".format(job.status, job.retcode))
job.logfile.close()
if not my_opt_tmpdir and not setupmode:
- with open("%s/%s.xml" % (job.workdir, junit_filename), "w") as f:
+ with open("{}/{}.xml".format(job.workdir, junit_filename), "w") as f:
junit_errors = 1 if job.retcode == 16 else 0
junit_failures = 1 if job.retcode != 0 and junit_errors == 0 else 0
print('<?xml version="1.0" encoding="UTF-8"?>', file=f)
- print('<testsuites disabled="0" errors="%d" failures="%d" tests="1" time="%d">' % (junit_errors, junit_failures, job.total_time), file=f)
- print('<testsuite disabled="0" errors="%d" failures="%d" name="%s" skipped="0" tests="1" time="%d">' % (junit_errors, junit_failures, junit_ts_name, job.total_time), file=f)
+ print('<testsuites disabled="0" errors="{}" failures="{}" tests="1" time="{}">'.format(junit_errors, junit_failures, job.total_time), file=f)
+ print('<testsuite disabled="0" errors="{}" failures="{}" name="{}" skipped="0" tests="1" time="{}">'.format(junit_errors, junit_failures, junit_ts_name, job.total_time), file=f)
print('<properties>', file=f)
- print('<property name="os" value="%s"/>' % os.name, file=f)
+ print('<property name="os" value="{}"/>'.format(os.name), file=f)
print('</properties>', file=f)
- print('<testcase classname="%s" name="%s" status="%s" time="%d">' % (junit_ts_name, junit_tc_name, job.status, job.total_time), file=f)
+ print('<testcase classname="{}" name="{}" status="{}" time="{}">'.format(junit_ts_name, junit_tc_name, job.status, job.total_time), file=f)
if junit_errors:
- print('<error message="%s" type="%s"/>' % (job.status, job.status), file=f)
+ print('<error message="{}" type="{}"/>'.format(job.status, job.status), file=f)
if junit_failures:
- print('<failure message="%s" type="%s"/>' % (job.status, job.status), file=f)
+ print('<failure message="{}" type="{}"/>'.format(job.status, job.status), file=f)
print('<system-out>', end="", file=f)
- with open("%s/logfile.txt" % (job.workdir), "r") as logf:
+ with open("{}/logfile.txt".format(job.workdir), "r") as logf:
for line in logf:
print(line.replace("&", "&").replace("<", "<").replace(">", ">").replace("\"", """), end="", file=f)
print('</system-out></testcase></testsuite></testsuites>', file=f)
- with open("%s/status" % (job.workdir), "w") as f:
- print("%s %d %d" % (job.status, job.retcode, job.total_time), file=f)
+ with open("{}/status".format(job.workdir), "w") as f:
+ print("{{{} {} {}}}".format(job.status, job.retcode, job.total_time), file=f)
return job.retcode
if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)):
if self.logfile is not None:
print(line, file=self.logfile)
- self.job.log("%s: %s" % (self.info, line))
+ self.job.log("{}: {}".format(self.info, line))
def handle_exit(self, retcode):
if self.terminated:
if self.job.opt_wait and not timeout:
return
if self.running:
- self.job.log("%s: terminating process" % self.info)
+ self.job.log("{}: terminating process".format(self.info))
if os.name == "posix":
os.killpg(self.p.pid, signal.SIGTERM)
self.p.terminate()
if not dep.finished:
return
- self.job.log("%s: starting process \"%s\"" % (self.info, self.cmdline))
+ self.job.log("{}: starting process \"{}\"".format(self.info, self.cmdline))
if os.name == "posix":
def preexec_fn():
self.handle_output(outs)
if self.p.poll() is not None:
- self.job.log("%s: finished (returncode=%d)" % (self.info, self.p.returncode))
+ self.job.log("{}: finished (returncode={})".format(self.info, self.p.returncode))
self.job.tasks_running.remove(self)
all_tasks_running.remove(self)
self.running = False
if self.p.returncode == 127:
self.job.status = "ERROR"
- self.job.log("%s: COMMAND NOT FOUND. ERROR." % self.info)
+ self.job.log("{}: COMMAND NOT FOUND. ERROR.".format(self.info))
self.terminated = True
self.job.terminate()
return
if self.checkretcode and self.p.returncode != 0:
self.job.status = "ERROR"
- self.job.log("%s: job failed. ERROR." % self.info)
+ self.job.log("{}: job failed. ERROR.".format(self.info))
self.terminated = True
self.job.terminate()
return
self.summary = list()
- self.logfile = open("%s/logfile.txt" % workdir, "a")
+ self.logfile = open("{}/logfile.txt".format(workdir), "a")
for line in early_logs:
print(line, file=self.logfile, flush=True)
if not reusedir:
- with open("%s/config.sby" % workdir, "w") as f:
+ with open("{}/config.sby".format(workdir), "w") as f:
for line in sbyconfig:
print(line, file=f)
if self.opt_timeout is not None:
total_clock_time = int(time() - self.start_clock_time)
if total_clock_time > self.opt_timeout:
- self.log("Reached TIMEOUT (%d seconds). Terminating all tasks." % self.opt_timeout)
+ self.log("Reached TIMEOUT ({} seconds). Terminating all tasks.".format(self.opt_timeout))
self.status = "TIMEOUT"
self.terminate(timeout=True)
def log(self, logmessage):
tm = localtime()
- print("SBY %2d:%02d:%02d [%s] %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
- print("SBY %2d:%02d:%02d [%s] %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
+ print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
+ print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
def error(self, logmessage):
tm = localtime()
- print("SBY %2d:%02d:%02d [%s] ERROR: %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
- print("SBY %2d:%02d:%02d [%s] ERROR: %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
+ print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
+ print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
self.status = "ERROR"
if "ERROR" not in self.expect:
self.retcode = 16
self.terminate()
- with open("%s/%s" % (self.workdir, self.status), "w") as f:
- print("ERROR: %s" % logmessage, file=f)
+ with open("{}/{}".format(self.workdir, self.status), "w") as f:
+ print("ERROR: {}".format(logmessage), file=f)
raise SbyAbort(logmessage)
def makedirs(self, path):
for dstfile, lines in self.verbatim_files.items():
dstfile = self.workdir + "/src/" + dstfile
- self.log("Writing '%s'." % dstfile)
+ self.log("Writing '{}'.".format(dstfile))
with open(dstfile, "w") as f:
for line in lines:
for dstfile, srcfile in self.files.items():
if dstfile.startswith("/") or dstfile.startswith("../") or ("/../" in dstfile):
- self.error("destination filename must be a relative path without /../: %s" % dstfile)
+ self.error("destination filename must be a relative path without /../: {}".format(dstfile))
dstfile = self.workdir + "/src/" + dstfile
srcfile = process_filename(srcfile)
if basedir != "" and not os.path.exists(basedir):
os.makedirs(basedir)
- self.log("Copy '%s' to '%s'." % (srcfile, dstfile))
+ self.log("Copy '{}' to '{}'.".format(srcfile, dstfile))
copyfile(srcfile, dstfile)
def handle_str_option(self, option_name, default_value):
def handle_bool_option(self, option_name, default_value):
if option_name in self.options:
if self.options[option_name] not in ["on", "off"]:
- self.error("Invalid value '%s' for boolean option %s." % (self.options[option_name], option_name))
+ self.error("Invalid value '{}' for boolean option {}.".format(self.options[option_name], option_name))
self.__dict__["opt_" + option_name] = self.options[option_name] == "on"
self.used_options.add(option_name)
else:
self.__dict__["opt_" + option_name] = default_value
def make_model(self, model_name):
- if not os.path.isdir("%s/model" % self.workdir):
- os.makedirs("%s/model" % self.workdir)
+ if not os.path.isdir("{}/model".format(self.workdir)):
+ os.makedirs("{}/model".format(self.workdir))
if model_name in ["base", "nomem"]:
- with open("%s/model/design%s.ys" % (self.workdir, "" if model_name == "base" else "_nomem"), "w") as f:
- print("# running in %s/src/" % self.workdir, file=f)
+ with open("{}/model/design{}.ys".format(self.workdir, "" if model_name == "base" else "_nomem"), "w") as f:
+ print("# running in {}/src/".format(self.workdir), file=f)
for cmd in self.script:
print(cmd, file=f)
if model_name == "base":
print("opt -keepdc -fast", file=f)
print("check", file=f)
print("hierarchy -simcheck", file=f)
- print("write_ilang ../model/design%s.il" % ("" if model_name == "base" else "_nomem"), file=f)
+ print("write_ilang ../model/design{}.il".format("" if model_name == "base" else "_nomem"), file=f)
task = SbyTask(self, model_name, [],
- "cd %s/src; %s -ql ../model/design%s.log ../model/design%s.ys" % (self.workdir, self.exe_paths["yosys"],
- "" if model_name == "base" else "_nomem", "" if model_name == "base" else "_nomem"))
+ "cd {}/src; {} -ql ../model/design{s}.log ../model/design{s}.ys".format(self.workdir, self.exe_paths["yosys"],
+ s="" if model_name == "base" else "_nomem"))
task.checkretcode = True
return [task]
if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", 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)
+ with open("{}/model/design_{}.ys".format(self.workdir, model_name), "w") as f:
+ print("# running in {}/model/".format(self.workdir), file=f)
+ print("read_ilang design{}.il".format("_nomem" if "_nomem" in model_name else ""), file=f)
if "_syn" in model_name:
print("techmap", file=f)
print("opt -fast", file=f)
print("opt_clean", file=f)
print("stat", file=f)
if "_stbv" in model_name:
- print("write_smt2 -stbv -wires design_%s.smt2" % model_name, file=f)
+ print("write_smt2 -stbv -wires design_{}.smt2".format(model_name), file=f)
elif "_stdt" in model_name:
- print("write_smt2 -stdt -wires design_%s.smt2" % model_name, file=f)
+ print("write_smt2 -stdt -wires design_{}.smt2".format(model_name), file=f)
else:
- print("write_smt2 -wires design_%s.smt2" % model_name, file=f)
+ print("write_smt2 -wires design_{}.smt2".format(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))
+ "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name))
task.checkretcode = True
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)
+ with open("{}/model/design_{}.ys".format(self.workdir, model_name), "w") as f:
+ print("# running in {}/model/".format(self.workdir), file=f)
+ print("read_ilang design{}.il".format("_nomem" if "_nomem" in model_name else ""), file=f)
print("flatten", file=f)
print("setundef -undriven -anyseq", file=f)
print("setattr -unset keep", 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)
+ print("write_btor design_{}.btor".format(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))
+ "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=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)
+ with open("{}/model/design_aiger.ys".format(self.workdir), "w") as f:
+ print("# running in {}/model/".format(self.workdir), file=f)
print("read_ilang design_nomem.il", file=f)
print("flatten", file=f)
print("setundef -undriven -anyseq", file=f)
print("write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig", file=f)
task = SbyTask(self, "aig", self.model("nomem"),
- "cd %s/model; %s -ql design_aiger.log design_aiger.ys" % (self.workdir, self.exe_paths["yosys"]))
+ "cd {}/model; {} -ql design_aiger.log design_aiger.ys".format(self.workdir, self.exe_paths["yosys"]))
task.checkretcode = True
return [task]
mode = None
key = None
- with open("%s/config.sby" % self.workdir, "r") as f:
+ with open("{}/config.sby".format(self.workdir), "r") as f:
for line in f:
raw_line = line
if mode in ["options", "engines", "files"]:
if match:
entries = match.group(1).split()
if len(entries) == 0:
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
if entries[0] == "options":
mode = "options"
if len(self.options) != 0 or len(entries) != 1:
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
continue
if entries[0] == "engines":
mode = "engines"
if len(self.engines) != 0 or len(entries) != 1:
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
continue
if entries[0] == "script":
mode = "script"
if len(self.script) != 0 or len(entries) != 1:
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
continue
if entries[0] == "file":
mode = "file"
if len(entries) != 2:
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
current_verbatim_file = entries[1]
if current_verbatim_file in self.verbatim_files:
- self.error("duplicate file: %s" % entries[1])
+ self.error("duplicate file: {}".format(entries[1]))
self.verbatim_files[current_verbatim_file] = list()
continue
if entries[0] == "files":
mode = "files"
if len(entries) != 1:
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
continue
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
if mode == "options":
entries = line.split()
if len(entries) != 2:
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
self.options[entries[0]] = entries[1]
continue
elif len(entries) == 2:
self.files[entries[0]] = entries[1]
else:
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
continue
if mode == "file":
self.verbatim_files[current_verbatim_file].append(raw_line)
continue
- self.error("sby file syntax error: %s" % line)
+ self.error("sby file syntax error: {}".format(line))
self.handle_str_option("mode", None)
if self.opt_mode not in ["bmc", "prove", "cover", "live"]:
- self.error("Invalid mode: %s" % self.opt_mode)
+ self.error("Invalid mode: {}".format(self.opt_mode))
self.expect = ["PASS"]
if "expect" in self.options:
for s in self.expect:
if s not in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]:
- self.error("Invalid expect value: %s" % s)
+ self.error("Invalid expect value: {}".format(s))
self.handle_bool_option("multiclock", False)
self.handle_bool_option("wait", False)
self.error("Config file is lacking engine configuration.")
if self.reusedir:
- rmtree("%s/model" % self.workdir, ignore_errors=True)
+ rmtree("{}/model".format(self.workdir), ignore_errors=True)
else:
self.copy_src()
for opt in self.options.keys():
if opt not in self.used_options:
- self.error("Unused option: %s" % opt)
+ self.error("Unused option: {}".format(opt))
self.taskloop()
self.total_time = total_process_time
self.summary = [
- "Elapsed clock time [H:MM:SS (secs)]: %d:%02d:%02d (%d)" %
+ "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
(total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time),
- "Elapsed process time [H:MM:SS (secs)]: %d:%02d:%02d (%d)" %
+ "Elapsed process time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
(total_process_time // (60*60), (total_process_time // 60) % 60, total_process_time % 60, total_process_time),
] + self.summary
else:
self.summary = [
- "Elapsed clock time [H:MM:SS (secs)]: %d:%02d:%02d (%d)" %
+ "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
(total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time),
"Elapsed process time unvailable on Windows"
] + self.summary
for line in self.summary:
- self.log("summary: %s" % line)
+ self.log("summary: {}".format(line))
assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]
if self.status == "TIMEOUT": self.retcode = 8
if self.status == "ERROR": self.retcode = 16
- with open("%s/%s" % (self.workdir, self.status), "w") as f:
+ with open("{}/{}".format(self.workdir, self.status), "w") as f:
for line in self.summary:
print(line, file=f)
if abc_command[0] == "bmc3":
if mode != "bmc":
job.error("ABC command 'bmc3' is only valid in bmc mode.")
- abc_command[0] += " -F %d -v" % job.opt_depth
+ abc_command[0] += " -F {} -v".format(job.opt_depth)
elif abc_command[0] == "sim3":
if mode != "bmc":
job.error("ABC command 'sim3' is only valid in bmc mode.")
- abc_command[0] += " -F %d -v" % job.opt_depth
+ abc_command[0] += " -F {} -v".format(job.opt_depth)
elif abc_command[0] == "pdr":
if mode != "prove":
job.error("ABC command 'pdr' is only valid in prove mode.")
else:
- job.error("Invalid ABC command %s." % abc_command[0])
+ job.error("Invalid ABC command {}.".format(abc_command[0]))
- task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"),
- ("cd %s; %s -c 'read_aiger model/design_aiger.aig; fold; strash; %s; write_cex -a engine_%d/trace.aiw'") %
+ task = SbyTask(job, "engine_{}".format(engine_idx), job.model("aig"),
+ ("cd {}; {} -c 'read_aiger model/design_aiger.aig; fold; strash; {}; write_cex -a engine_{}/trace.aiw'").format
(job.workdir, job.exe_paths["abc"], " ".join(abc_command), engine_idx),
- logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w"))
+ logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w"))
task.noprintregex = re.compile(r"^\.+$")
task_status = None
assert task_status is not None
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.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status))
+ job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status))
job.terminate()
if task_status == "FAIL" and job.opt_aigsmt != "none":
- 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_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") %
+ task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"),
+ ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
+ "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format
(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"))
+ "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop),
+ job.opt_append, i=engine_idx, engine_idx, engine_idx, engine_idx),
+ logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w"))
task2_status = None
assert task2_status is not None
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))
+ if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)):
+ job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx))
task2.output_callback = output_callback2
task2.exit_callback = exit_callback2
task.output_callback = output_callback
task.exit_callback = exit_callback
-
solver_cmd = " ".join([job.exe_paths["aigbmc"]] + solver_args[1:])
else:
- job.error("Invalid solver command %s." % solver_args[0])
+ job.error("Invalid solver command {}.".format(solver_args[0]))
- task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"),
- "cd %s; %s model/design_aiger.aig" % (job.workdir, solver_cmd),
- logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w"))
+ task = SbyTask(job, "engine_{}".format(engine_idx), job.model("aig"),
+ "cd {}; {} model/design_aiger.aig".format(job.workdir, solver_cmd),
+ logfile=open("{}/engine_{}/logfile.txt".format(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")
+ aiw_file = open("{}/engine_{}/trace.aiw".format(job.workdir, engine_idx), "w")
def output_callback(line):
nonlocal task_status
return None
if line.startswith("u"):
- return "No CEX up to depth %d." % (int(line[1:])-1)
+ return "No CEX up to depth {}.".format(int(line[1:])-1)
if line in ["0", "1", "2"]:
print(line, file=aiw_file)
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.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status))
+ job.summary.append("engine_{} ({}) returned {}".format(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_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") %
+ task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"),
+ ("cd {}; {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
+ "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
(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"))
+ "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop),
+ i=engine_idx),
+ logfile=open("{}/engine_{}/logfile2.txt".format(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_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") %
+ task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"),
+ ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
+ "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format
(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"))
+ "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop),
+ job.opt_append, i=engine_idx),
+ logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w"))
task2_status = None
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))
+ if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)):
+ job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(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)
+ job.log("engine_{}: Engine did not produce a counter example.".format(engine_idx))
task.output_callback = output_callback
task.exit_callback = exit_callback
-
job.error("Unexpected BTOR engine options.")
if solver_args[0] == "btormc":
- solver_cmd = job.exe_paths["btormc"] + " --stop-first -v 1 -kmax %d" % (job.opt_depth - 1)
+ solver_cmd = job.exe_paths["btormc"] + " --stop-first -v 1 -kmax {}".format(job.opt_depth - 1)
if job.opt_skip is not None:
- solver_cmd += " -kmin %d" % job.opt_skip
+ solver_cmd += " -kmin {}".format(job.opt_skip)
solver_cmd += " ".join([""] + solver_args[1:])
else:
- job.error("Invalid solver command %s." % solver_args[0])
+ job.error("Invalid solver command {}.".format(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 = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"),
+ "cd {}; {} model/design_btor.btor".format(job.workdir, solver_cmd),
+ logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w"))
task_status = None
produced_cex = False
end_of_cex = False
- wit_file = open("%s/engine_%d/trace.wit" % (job.workdir, engine_idx), "w")
+ wit_file = open("{}/engine_{}/trace.wit".format(job.workdir, engine_idx), "w")
def output_callback(line):
nonlocal task_status
end_of_cex = True
if line.startswith("u"):
- return "No CEX up to depth %d." % (int(line[1:])-1)
+ return "No CEX up to depth {}.".format(int(line[1:])-1)
if solver_args[0] == "btormc":
if "calling BMC on" in line:
wit_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.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status))
+ job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status))
job.terminate()
if produced_cex:
has_arrays = False
- with open("%s/model/design_btor.btor" % job.workdir, "r") as f:
+ with open("{}/model/design_btor.btor".format(job.workdir), "r") as f:
for line in f:
line = line.split()
if len(line) == 5 and line[1] == "sort" and line[2] == "array":
break
if has_arrays:
- setupcmd = "cd %s;" % (job.workdir)
- finalwit = "engine_%d/trace.wit" % engine_idx
+ setupcmd = "cd {};".format(job.workdir)
+ finalwit = "engine_{}/trace.wit".format(engine_idx)
else:
- setupcmd = "cd %s; { echo sat; btorsim --states model/design_btor.btor engine_%d/trace.wit; } > engine_%d/simtrace.wit &&" % (job.workdir, engine_idx, engine_idx)
- finalwit = "engine_%d/simtrace.wit" % engine_idx
+ setupcmd = "cd {}; { echo sat; btorsim --states model/design_btor.btor engine_{i}/trace.wit; } > engine_{i}/simtrace.wit &&".format(job.workdir, i=engine_idx)
+ finalwit = "engine_{}/simtrace.wit".format(engine_idx)
if mode == "live":
- task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
- ("%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 --btorwit %s model/design_smt2.smt2") %
- (setupcmd, 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, finalwit),
- logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
+ task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"),
+ ("{} {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
+ "--dump-smtc engine_{i}/trace.smtc --btorwit {} model/design_smt2.smt2").format(setupcmd, job.exe_paths["smtbmc"], job.opt_aigsmt, "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), finalwit, i=engine_idx),
+ logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w"))
else:
- task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
- ("%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 --btorwit %s model/design_smt2.smt2") %
+ task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"),
+ ("{} {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " +
+ "--dump-smtc engine_{i}/trace.smtc --btorwit {} model/design_smt2.smt2").format
(setupcmd, 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, finalwit),
- logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w"))
+ "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop),
+ job.opt_append, finalwit, i=engine_idx),
+ logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w"))
task2_status = None
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))
+ if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)):
+ job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(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)
+ job.log("engine_{}: Engine did not produce a counter example.".format(engine_idx))
task.output_callback = output_callback
task.exit_callback = exit_callback
-
job.error("smtbmc options --basecase and --induction are exclusive.")
induction_only = True
else:
- job.error("Invalid smtbmc options %s." % o)
+ job.error("Invalid smtbmc options {}.".format(o))
xtra_opts = False
for i, a in enumerate(args):
smtbmc_opts += ["--unroll"]
if job.opt_smtc is not None:
- smtbmc_opts += ["--smtc", "src/%s" % job.opt_smtc]
+ smtbmc_opts += ["--smtc", "src/{}".format(job.opt_smtc)]
if job.opt_tbtop is not None:
smtbmc_opts += ["--vlogtb-top", job.opt_tbtop]
run("prove_induction", job, engine_idx, engine)
return
- taskname = "engine_%d" % engine_idx
- trace_prefix = "engine_%d/trace" % engine_idx
- logfile_prefix = "%s/engine_%d/logfile" % (job.workdir, engine_idx)
+ taskname = "engine_{}".format(engine_idx)
+ trace_prefix = "engine_{}/trace".format(engine_idx)
+ logfile_prefix = "{}/engine_{}/logfile".format(job.workdir, engine_idx)
if mode == "prove_basecase":
taskname += ".basecase"
if job.opt_skip is not None:
- t_opt = "%d:%d" % (job.opt_skip, job.opt_depth)
+ t_opt = "{}:{}".format(job.opt_skip, job.opt_depth)
else:
- t_opt = "%d" % job.opt_depth
+ t_opt = "{}".format(job.opt_depth)
task = SbyTask(job, taskname, job.model(model_name),
- "cd %s; %s %s -t %s --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" %
- (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name),
+ "cd {}; {} {} -t {} --append {} --dump-vcd {p}.vcd --dump-vlogtb {p}_tb.v --dump-smtc {p}.smtc model/design_{}.smt2".format
+ (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, job.opt_append, model_name, p=trace_prefix),
logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress))
if mode == "prove_basecase":
def exit_callback(retcode):
if task_status is None:
- job.error("engine_%d: Engine terminated without status." % engine_idx)
+ job.error("engine_{}: Engine terminated without status.".format(engine_idx))
if mode == "bmc" or mode == "cover":
job.update_status(task_status)
task_status_lower = task_status.lower() if task_status == "PASS" else task_status
- job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status_lower))
- job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status_lower))
+ job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status_lower))
+ job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status_lower))
if task_status == "FAIL" and mode != "cover":
- 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))
+ if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)):
+ job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx))
job.terminate()
elif mode in ["prove_basecase", "prove_induction"]:
task_status_lower = task_status.lower() if task_status == "PASS" else task_status
- job.log("engine_%d: Status returned by engine for %s: %s" % (engine_idx, mode.split("_")[1], task_status_lower))
- job.summary.append("engine_%d (%s) returned %s for %s" % (engine_idx, " ".join(engine), task_status_lower, mode.split("_")[1]))
+ job.log("engine_{}: Status returned by engine for {}: {}".format(engine_idx, mode.split("_")[1], task_status_lower))
+ job.summary.append("engine_{} ({}) returned {} for {}".format(engine_idx, " ".join(engine), task_status_lower, mode.split("_")[1]))
if mode == "prove_basecase":
for task in job.basecase_tasks:
else:
job.update_status(task_status)
- 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))
+ if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)):
+ job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx))
job.terminate()
elif mode == "prove_induction":
task.output_callback = output_callback
task.exit_callback = exit_callback
-
-
engine = job.engines[engine_idx]
assert len(engine) > 0
- job.log("engine_%d: %s" % (engine_idx, " ".join(engine)))
- job.makedirs("%s/engine_%d" % (job.workdir, engine_idx))
+ job.log("engine_{}: {}".format(engine_idx, " ".join(engine)))
+ job.makedirs("{}/engine_{}".format(job.workdir, engine_idx))
if engine[0] == "smtbmc":
import sby_engine_smtbmc
sby_engine_btor.run("bmc", job, engine_idx, engine)
else:
- job.error("Invalid engine '%s' for bmc mode." % engine[0])
-
+ job.error("Invalid engine '{}' for bmc mode.".format(engine[0]))
engine = job.engines[engine_idx]
assert len(engine) > 0
- job.log("engine_%d: %s" % (engine_idx, " ".join(engine)))
- job.makedirs("%s/engine_%d" % (job.workdir, engine_idx))
+ job.log("engine_{}: {}".format(engine_idx, " ".join(engine)))
+ job.makedirs("{}/engine_{}".format(job.workdir, engine_idx))
if engine[0] == "smtbmc":
import sby_engine_smtbmc
sby_engine_smtbmc.run("cover", job, engine_idx, engine)
else:
- job.error("Invalid engine '%s' for cover mode." % engine[0])
-
+ job.error("Invalid engine '{}' for cover mode.".format(engine[0]))
engine = job.engines[engine_idx]
assert len(engine) > 0
- job.log("engine_%d: %s" % (engine_idx, " ".join(engine)))
- job.makedirs("%s/engine_%d" % (job.workdir, engine_idx))
+ job.log("engine_{}: {}".format(engine_idx, " ".join(engine)))
+ job.makedirs("{}/engine_{}".format(job.workdir, engine_idx))
if engine[0] == "aiger":
import sby_engine_aiger
sby_engine_aiger.run("live", job, engine_idx, engine)
else:
- job.error("Invalid engine '%s' for live mode." % engine[0])
-
+ job.error("Invalid engine '{}' for live mode.".format(engine[0]))
engine = job.engines[engine_idx]
assert len(engine) > 0
- job.log("engine_%d: %s" % (engine_idx, " ".join(engine)))
- job.makedirs("%s/engine_%d" % (job.workdir, engine_idx))
+ job.log("engine_{}: {}".format(engine_idx, " ".join(engine)))
+ job.makedirs("{}/engine_{}".format(job.workdir, engine_idx))
if engine[0] == "smtbmc":
import sby_engine_smtbmc
sby_engine_abc.run("prove", job, engine_idx, engine)
else:
- job.error("Invalid engine '%s' for prove mode." % engine[0])
-
+ job.error("Invalid engine '{}' for prove mode.".format(engine[0]))
projects / SymbiYosys.git / commitdiff