diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 29056f3..d3dae3f 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -129,58 +129,71 @@ Mode Description 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) | -+------------------+------------+---------------------------------------------------------+ -| ``multiclock`` | All | Create a model with multiple clocks and/or asynchronous | -| | | logic. Values: ``on``, ``off``. Default: ``off`` | -+------------------+------------+---------------------------------------------------------+ -| ``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`` | -+------------------+------------+---------------------------------------------------------+ -| ``vcd`` | All | Write VCD traces for counter-example or cover traces. | -| | | Values: ``on``, ``off``. Default: ``on`` | -+------------------+------------+---------------------------------------------------------+ -| ``aigsmt`` | All | Which SMT2 solver to use for converting AIGER witnesses | -| | | to counter example traces. Use ``none`` to disable | -| | | conversion of AIGER witnesses. Default: ``yices`` | -+------------------+------------+---------------------------------------------------------+ -| ``tbtop`` | All | The top module for generated Verilog test benches, as | -| | | hierarchical path relative to the design top module. | -+------------------+------------+---------------------------------------------------------+ -| ``make_model`` | All | Force generation of the named formal models. Takes a | -| | | comma-separated list of model names. For a model | -| | | ```` this will generate the | -| | | ``model/design_.*`` files within the working | -| | | directory, even when not required to run the task. | -+------------------+------------+---------------------------------------------------------+ -| ``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`` | -+------------------+------------+---------------------------------------------------------+ -| ``skip`` | ``bmc``, | Skip the specified number of time steps. Only valid | -| | ``cover`` | with smtbmc engine. All other engines are disabled when | -| | | this option is used. Default: None | -+------------------+------------+---------------------------------------------------------+ -| ``append`` | ``bmc``, | When generating a counter-example trace, add the | -| | ``prove``, | specified number of cycles at the end of the trace. | -| | ``cover`` | Default: ``0`` | -+------------------+------------+---------------------------------------------------------+ ++-------------------+------------+---------------------------------------------------------+ +| 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) | ++-------------------+------------+---------------------------------------------------------+ +| ``multiclock`` | All | Create a model with multiple clocks and/or asynchronous | +| | | logic. Values: ``on``, ``off``. Default: ``off`` | ++-------------------+------------+---------------------------------------------------------+ +| ``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`` | ++-------------------+------------+---------------------------------------------------------+ +| ``vcd`` | All | Write VCD traces for counter-example or cover traces. | +| | | Values: ``on``, ``off``. Default: ``on`` | ++-------------------+------------+---------------------------------------------------------+ +| ``vcd_sim`` | All | When generating VCD traces, use Yosys's ``sim`` | +| | | command. Replaces the engine native VCD output. | +| | | Values: ``on``, ``off``. Default: ``off`` | ++-------------------+------------+---------------------------------------------------------+ +| ``fst`` | All | Generate FST traces using Yosys's sim command. | +| | | Values: ``on``, ``off``. Default: ``off`` | ++-------------------+------------+---------------------------------------------------------+ +| ``aigsmt`` | All | Which SMT2 solver to use for converting AIGER witnesses | +| | | to counter example traces. Use ``none`` to disable | +| | | conversion of AIGER witnesses. Default: ``yices`` | ++-------------------+------------+---------------------------------------------------------+ +| ``tbtop`` | All | The top module for generated Verilog test benches, as | +| | | hierarchical path relative to the design top module. | ++-------------------+------------+---------------------------------------------------------+ +| ``make_model`` | All | Force generation of the named formal models. Takes a | +| | | comma-separated list of model names. For a model | +| | | ```` this will generate the | +| | | ``model/design_.*`` files within the working | +| | | directory, even when not required to run the task. | ++-------------------+------------+---------------------------------------------------------+ +| ``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`` | ++-------------------+------------+---------------------------------------------------------+ +| ``skip`` | ``bmc``, | Skip the specified number of time steps. Only valid | +| | ``cover`` | with smtbmc engine. All other engines are disabled when | +| | | this option is used. Default: None | ++-------------------+------------+---------------------------------------------------------+ +| ``append`` | ``bmc``, | When generating a counter-example trace, add the | +| | ``prove``, | specified number of cycles at the end of the trace. | +| | ``cover`` | Default: ``0`` | ++-------------------+------------+---------------------------------------------------------+ +| ``append_assume`` | ``bmc``, | Uphold assumptions when appending cycles at the end of | +| | ``prove``, | the trace. Depending on the engine and options used | +| | ``cover`` | this may be implicitly on or not supported (as | +| | | indicated in SBY's log output). | +| | | Values: ``on``, ``off``. Default: ``off`` | ++-------------------+------------+---------------------------------------------------------+ Engines section ---------------