Use "hierarchy -simcheck" in default script

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index a18687bd7feb8bf88b48c62158b9fb221a3d73ce..2d12ef77fe9920006d8582f14ec23a4935b06d96 100644 (file)
--- 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 23ec6938413d4e0c84a67c806ec03702cf2625ba..525f94d498e787aa62d01bbc8db0c2f9b1afcf8c 100644 (file)
--- 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)