Add docs for "wait" option, more config checking

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index cc2bf53529b0c30fd1db9ef1a0852642f66a1c12..31d78bffcd1badb9df638b9370d723dde8b6a3a1 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -34,6 +34,10 @@ options are:
 +-------------+-----------+---------------------------------------------------------+
 | ``timeout`` |   All     | Timeout in seconds. Default: ``none`` (i.e. no timeout) |
 +-------------+-----------+---------------------------------------------------------+
+| ``wait``    |   All     | Instead of terminating when the first engine returns,   |
+|             |           | wait for all engines to return and check for            |
+|             |           | consistency. Values: ``on``, ``off``. Default: ``off``  |
++-------------+-----------+---------------------------------------------------------+
 | ``depth``   | ``bmc``,  | Depth of the bounded model check. Only the specified    |
 |             | ``cover`` | number of cycles are considered. Default: ``20``        |
 |             +-----------+---------------------------------------------------------+

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 01723d37a1512c341775dd770637fb6ad1211340..9a7da46d9adc3e64b0fed8b6e77c8c8a950745c2 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -129,9 +129,7 @@ class SbyJob:
         self.files = dict()
         self.models = dict()
         self.workdir = workdir
-
         self.status = "UNKNOWN"
-        self.expect = ["PASS"]
 
         self.tasks_running = []
         self.tasks_all = []
@@ -363,12 +361,18 @@ class SbyJob:
 
     def run(self):
         assert "mode" in self.options
+        assert self.options["mode"] in ["bmc", "prove", "cover"]
 
+        self.expect = ["PASS"]
         if "expect" in self.options:
             self.expect = self.options["expect"].upper().split(",")
 
+        for s in self.expect:
+            assert s in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]
+
         self.waitmode = False
         if "wait" in self.options:
+            assert self.options["wait"] in ["on", "off"]
             self.waitmode = self.options["wait"] == "on"
 
         self.copy_src()