diff --git a/docs/source/reference.rst b/docs/source/reference.rst index c06d6c0..417a065 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -124,6 +124,7 @@ Mode Description ``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 +``prep`` Prepare the design and write the preprocessed model without running solver engines ========= =========== .. @@ -176,6 +177,9 @@ options are: | | | ``model/design_.*`` files within the working | | | | directory, even when not required to run the task. | +-------------------+------------+---------------------------------------------------------+ +| ``skip_prep`` | All | Skip SBY's internal preparation step. Values: ``on``, | +| | | ``off``. Default: ``off`` | ++-------------------+------------+---------------------------------------------------------+ | ``smtc`` | ``bmc``, | Pass this ``.smtc`` file to the smtbmc engine. All | | | ``prove``, | other engines are disabled when this option is used. | | | ``cover`` | Default: None |