From d24d7e1aef1eac422ae40a4512f8849fd5fae124 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 12 May 2018 14:03:37 +0200 Subject: [PATCH] Use "hierarchy -simcheck" in default script Signed-off-by: Clifford Wolf --- sbysrc/sby_core.py | 1 + sbysrc/sby_engine_smtbmc.py | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index a18687b..2d12ef7 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -300,6 +300,7 @@ class SbyJob: print("setundef -anyseq", file=f) 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) task = SbyTask(self, model_name, [], diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 23ec693..525f94d 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -146,7 +146,8 @@ def run(mode, job, engine_idx, engine): return line def exit_callback(retcode): - assert task_status is not None + if task_status is None: + job.error("engine_%d: Engine terminated without status." % engine_idx) if mode == "bmc" or mode == "cover": job.update_status(task_status) -- 2.30.2