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

Fixed "counterexample trace:" log message for things like warmup failed

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-08-21 14:00:30 +02:00
parent 2fef25f93d
commit f2697c23c0
3 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
sbysrc/sby_engine_abc.py
View file

@ -109,7 +109,8 @@ def run(mode, job, engine_idx, engine):
assert task2_status is not None
assert task2_status == "FAIL"
job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
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

3
sbysrc/sby_engine_aiger.py
View file

@ -128,7 +128,8 @@ def run(mode, job, engine_idx, engine):
else:
assert task2_status == "FAIL"
job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
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

6
sbysrc/sby_engine_smtbmc.py
View file

@ -155,7 +155,8 @@ def run(mode, job, engine_idx, engine):
job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status))
if task_status == "FAIL" and mode != "cover":
job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
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))
job.terminate()
@ -172,7 +173,8 @@ def run(mode, job, engine_idx, engine):
else:
job.update_status(task_status)
job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
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))
job.terminate()
elif mode == "prove_induction":