diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 710ba7b..4af5e0a 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -178,6 +178,9 @@ options are: | | ``prove``, | specified number of cycles at the end of the trace. | | | ``cover`` | Default: ``0`` | +------------------+------------+---------------------------------------------------------+ +| ``stage`` | All | The stages to select to run. | +| | | Default: All | ++------------------+------------+---------------------------------------------------------+ Engines section --------------- @@ -205,6 +208,19 @@ solver options. In the 2nd line ``abc`` is the engine, there are no engine options, ``sim3`` is the solver, and ``-W 15`` are solver options. + +The ``[engines]`` section also takes an argument as to what mode that block applies to. +Meaning you can specify an engine block for a given mode. + +Example: + +.. code-block:: text + + [engines bmc] + btor pono + abc sim3 + + The following mode/engine/solver combinations are currently supported: +-----------+--------------------------+ @@ -391,6 +407,48 @@ Run ``yosys`` in a terminal window and enter ``help`` on the Yosys prompt for a command list. Run ``help `` for a detailed description of the command, for example ``help prep``. +Setup section +------------- + +The ``[setup]`` section provides a way to add global cutpoints, and enable/disable/assume/define patterns. +By default properties that are unspecified default to enabled, and a ``disable *`` at the end of the settings +will set the default to be disabled. + +For example: + +.. code-block:: text + + [setup] + enable * + +The following options are available for the ``[setup]`` section: + +.. todo:: + + Document better + ++------------------+---------------------------------------------------------+ +| Option | Description | ++==================+=========================================================+ +| ``cutpoint`` | Defines a cutpoint pattern. | ++------------------+---------------------------------------------------------+ +| ``disable`` | Defines a disable pattern. | ++------------------+---------------------------------------------------------+ +| ``enable`` | Defines an enable pattern. | ++------------------+---------------------------------------------------------+ +| ``assume`` | Defines an assume pattern. | ++------------------+---------------------------------------------------------+ +| ``define`` | Define a value. | ++------------------+---------------------------------------------------------+ + + +Stage section +------------- + +.. todo:: + + Document + Files section ------------- diff --git a/tests/parser/options.sby b/tests/parser/options.sby deleted file mode 100644 index bf6a553..0000000 --- a/tests/parser/options.sby +++ /dev/null @@ -1,8 +0,0 @@ -[options] -mode bmc -depth 1 -expect error -stages foo,bar,nya - -[engines] -smtbmc