From: Clifford Wolf Date: Wed, 1 Mar 2017 10:09:30 +0000 (+0100) Subject: Update docs X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7fdbb4c1793f3b2643647a77bed99314c5f9eeaa;p=SymbiYosys.git Update docs --- diff --git a/docs/source/index.rst b/docs/source/index.rst index b697dbe..ec6d8f6 100644 --- 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 31d78bf..5195c39 100644 --- 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 ---------------