Update docs

diff --git a/docs/source/index.rst b/docs/source/index.rst
index b697dbed87b4424b47abe21c1615105a835aa4a2..ec6d8f65f9ea7d658c5cca98d8b9955f3d81cd50 100644 (file)
--- a/docs/source/index.rst
+++ b/docs/source/index.rst
@@ -9,7 +9,7 @@ formal tasks:
    * Bounded verification of safety properties (assertions)
    * Unbounded verification of safety properties
    * Generation of test benches from cover statements
-   * Verification of liveness properties [TBD]
+   * Verification of liveness properties
    * Formal equivalence checking [TBD]
 
 (Items marked [TBD] are features under construction and not available

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 31d78bffcd1badb9df638b9370d723dde8b6a3a1..5195c3982ba5a3094f7b1a0c31c1b0a596c81e5b 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -16,35 +16,47 @@ option is mandatory. The possible values for the ``mode`` option are:
 ========= ===========
 Mode      Description
 ========= ===========
-``bmc``   Bounded model check to verify safety properties (assert() statements)
-``prove`` Unbounded model check to verify safety properties (assert() statements)
-``cover`` Generate set of shortest trace required to reach all cover() statements
+``bmc``   Bounded model check to verify safety properties (``assert(...)`` statements)
+``prove`` Unbounded model check to verify safety properties (``assert(...)`` statements)
+``live``  Unbounded model check to verify liveness properties (``assert(s_eventually ...)`` statements)
+``cover`` Generate set of shortest traces required to reach all cover() statements
 ========= ===========
 
 All other options have default values and thus are optional. The available
 options are:
 
-+-------------+-----------+---------------------------------------------------------+
-|   Option    |   Modes   | Description                                             |
-+=============+===========+=========================================================+
-| ``expect``  |   All     | Expected result as comma-separated list of the tokens   |
-|             |           | ``pass``, ``fail``, ``unknown``, ``error``, and         |
-|             |           | ``timeout``. Unexpected results yield a nonzero return  |
-|             |           | code . Default: ``pass``                                |
-+-------------+-----------+---------------------------------------------------------+
-| ``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``        |
-|             +-----------+---------------------------------------------------------+
-|             | ``prove`` | Depth for the k-induction performed by the ``smtbmc``   |
-|             |           | engine. Other engines ignore this option in ``prove``   |
-|             |           | mode. Default: ``20``                                   |
-+-------------+-----------+---------------------------------------------------------+
++-------------+------------+---------------------------------------------------------+
+|   Option    |   Modes    | Description                                             |
++=============+============+=========================================================+
+| ``expect``  |   All      | Expected result as comma-separated list of the tokens   |
+|             |            | ``pass``, ``fail``, ``unknown``, ``error``, and         |
+|             |            | ``timeout``. Unexpected results yield a nonzero return  |
+|             |            | code . Default: ``pass``                                |
++-------------+------------+---------------------------------------------------------+
+| ``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``  |
++-------------+------------+---------------------------------------------------------+
+| ``aigsmt``  |   All      | Which SMT2 solver to use for converting AIGER witnesses |
+|             |            | to counter example traces. Default: ``z3``              |
++-------------+------------+---------------------------------------------------------+
+| ``smtc``    | ``bmc``,   | Pass this ``.smtc`` file to the smtbmc engine. All      |
+|             | ``prove``, | other engines are disabled when this option is used.    |
+|             | ``cover``  | Default: None                                           |
++-------------+------------+---------------------------------------------------------+
+| ``depth``   | ``bmc``,   | Depth of the bounded model check. Only the specified    |
+|             | ``cover``  | number of cycles are considered. Default: ``20``        |
+|             +------------+---------------------------------------------------------+
+|             | ``prove``  | Depth for the k-induction performed by the ``smtbmc``   |
+|             |            | engine. Other engines ignore this option in ``prove``   |
+|             |            | mode. Default: ``20``                                   |
++-------------+------------+---------------------------------------------------------+
+| ``append``  | ``bmc``,   | When generating a counter-example trace, add the        |
+|             | ``prove``, | specified number of cycles at the end of the trace.     |
+|             | ``cover``  | Default: ``0``                                          |
++-------------+------------+---------------------------------------------------------+
 
 Engines section
 ---------------