mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 14:04:07 +00:00
Code Activity

Improve bmc task management

Browse source
This commit is contained in:
Clifford Wolf 2017-01-30 11:50:14 +01:00
parent 7ff38491c6
commit f173c703f9
2 changed files with 13 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
sbysrc/sby_bmc.py
View file

@ -69,13 +69,10 @@ def run_smtbmc(job, engine_idx, engine):
if job.status == "FAIL": if job.status == "FAIL":
job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
for t in job.engine_tasks: job.terminate()
if task is not t:
t.terminate()
task.output_callback = output_callback task.output_callback = output_callback
task.exit_callback = exit_callback task.exit_callback = exit_callback
job.engine_tasks.append(task)
def run_abc(job, engine_idx, engine): def run_abc(job, engine_idx, engine):
@ -108,9 +105,7 @@ def run_abc(job, engine_idx, engine):
job.log("engine_%d: Status returned by engine: %s" % (engine_idx, 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.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), job.status))
for t in job.engine_tasks: job.terminate()
if task is not t:
t.terminate()
if job.status == "FAIL": if job.status == "FAIL":
task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
@ -141,7 +136,6 @@ def run_abc(job, engine_idx, engine):
task.output_callback = output_callback task.output_callback = output_callback
task.exit_callback = exit_callback task.exit_callback = exit_callback
job.engine_tasks.append(task)
def run(job): def run(job):
@ -150,9 +144,6 @@ def run(job):
if "depth" in job.options: if "depth" in job.options:
job.opt_depth = int(job.options["depth"]) job.opt_depth = int(job.options["depth"])
job.status = "UNKNOWN"
job.engine_tasks = list()
for engine_idx in range(len(job.engines)): for engine_idx in range(len(job.engines)):
engine = job.engines[engine_idx] engine = job.engines[engine_idx]
assert len(engine) > 0 assert len(engine) > 0

17
sbysrc/sby_core.py
View file

@ -103,10 +103,10 @@ class SbyTask:
self.running = False self.running = False
if self.checkretcode and self.p.returncode != 0: if self.checkretcode and self.p.returncode != 0:
self.job.log("%s: job failed. terminate." % self.info) self.job.status = "ERROR"
self.job.log("%s: job failed. ERROR." % self.info)
self.terminated = True self.terminated = True
for task in self.job.tasks_running: self.job.terminate()
task.terminate()
return return
self.finished = True self.finished = True
@ -124,6 +124,7 @@ class SbyJob:
self.models = dict() self.models = dict()
self.workdir = workdir self.workdir = workdir
self.status = None
self.tasks_running = [] self.tasks_running = []
self.tasks_all = [] self.tasks_all = []
@ -318,6 +319,10 @@ class SbyJob:
self.models[model_name] = self.make_model(model_name) self.models[model_name] = self.make_model(model_name)
return self.models[model_name] return self.models[model_name]
def terminate(self):
for task in self.tasks_running:
task.terminate()
def run(self): def run(self):
assert "mode" in self.options assert "mode" in self.options
@ -345,10 +350,10 @@ class SbyJob:
for line in self.summary: for line in self.summary:
self.log("summary: %s" % line) self.log("summary: %s" % line)
self.log("DONE (%s)" % self.status)
assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
with open("%s/%s" % (self.workdir, self.status), "w") as f: with open("%s/%s" % (self.workdir, self.status), "w") as f:
for line in self.summary: for line in self.summary:
print(line, file=f) print(line, file=f)
self.log("DONE (%s)" % self.status)
assert self.status in ["PASS", "FAIL"]