Add engines documentation

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 7a4811225740c43cf715806de460567b80174292..c8951e5f2ec08d7a18ed3aec0dccae78251527be 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -67,7 +67,110 @@ options are:
 Engines section
 ---------------
 
-TBD
+The ``[engines]`` section configures which engines should be used to solve the
+given problem. Each line in the ``[engines]`` section specifies one engine. When
+more than one engine is specified then the result returned by the first engine
+to finish is used.
+
+Each engine configuration consists of an engine name followed by engine options,
+usually followed by a solver name and solver options.
+
+Example:
+
+.. code-block:: text
+
+   [engines]
+   smtbmc --syn --nopresat z3 rewriter.cache_all=true opt.enable_sat=true
+   abc sim3 -W 15
+
+In the first line ``smtbmc`` is the engine, ``--syn --nopresat`` are engine options,
+``z3`` is the solver, and ``rewriter.cache_all=true opt.enable_sat=true`` are
+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.
+
+``smtbmc`` engine
+~~~~~~~~~~~~~~~~~
+
+The ``smtbmc`` engine supports the ``bmc``, ``prove``, and ``cover`` modes and supports
+the following options:
+
++-----------------+---------------------------------------------------------+
+|   Option        | Description                                             |
++=================+=========================================================+
+| ``--nomem``     | Don't use the SMT theory of arrays to model memories.   |
+|                 | Instead synthesize memories to registers and address    |
+|                 | logic.                                                  |
++-----------------+---------------------------------------------------------+
+| ``--syn``       | Synthesize the circuit to a gate-level representation   |
+|                 | instead of using word-level SMT operators. This also    |
+|                 | runs some low-level logic optimization on the circuit.  |
++-----------------+---------------------------------------------------------+
+| ``--stbv``      | Use large bit vectors (instead of uninterpreted         |
+|                 | functions) to represent the circuit state.              |
++-----------------+---------------------------------------------------------+
+| ``--nopresat``  | Do not run "presat" SMT queries that make sure that     |
+|                 | assumptions are non-conflicting (and potentially        |
+|                 | warmup the SMT solver).                                 |
++-----------------+---------------------------------------------------------+
+| ``--unroll``,   | Disable/enable unrolling of the SMT problem. The        |
+| ``--nounroll``  | default value depends on the solver being used.         |
++-----------------+---------------------------------------------------------+
+| ``--dumpsmt2``  | Write the SMT2 trace to an additional output file.      |
+|                 | (Useful for benchmarking and troubleshooting.)          |
++-----------------+---------------------------------------------------------+
+
+Any SMT2 solver that is compatible with ``yosys-smtbmc`` can be passed as
+argument to the ``smtbmc`` engine. The solver options are passed to the solver
+as additional command line options.
+
+The following solvers are currently supported by ``yosys-smtbmc``:
+
+  * yices
+  * boolector
+  * z3
+  * mathsat
+  * cvc4
+
+``aiger`` engine
+~~~~~~~~~~~~~~~~
+
+The ``aiger`` engine is a generic front-end for hardware modelcheckers that are capable
+of processing AIGER files. The engine supports no engine options and supports the following
+solvers:
+
++-------------------------------+---------------------------------+
+|   Solver                      |   Modes                         |
++===============================+=================================+
+| ``suprove``                   |   ``prove``, ``live``           |
++-------------------------------+---------------------------------+
+| ``avy``                       |   ``prove``                     |
++-------------------------------+---------------------------------+
+| ``aigbmc``                    |   ``prove``, ``live``           |
++-------------------------------+---------------------------------+
+
+Solver options are passed to the solver as additional command line options.
+
+``abc`` engine
+~~~~~~~~~~~~~~
+
+The ``abc`` engine is a front-end for the functionality in Berkeley ABC. It
+currently supports no engine options and supports the following
+solvers:
+
++------------+-----------------+---------------------------------+
+|   Solver   |   Modes         |   ABC Command                   |
++============+=================+=================================+
+| ``bmc3``   |  ``bmc``        |  ``bmc3 -F <depth> -v``         |
++------------+-----------------+---------------------------------+
+| ``sim3``   |  ``bmc``        |  ``sim3 -F <depth> -v``         |
++------------+-----------------+---------------------------------+
+| ``pdr``    |  ``prove``      |  ``pdr``                        |
++------------+-----------------+---------------------------------+
+
+Solver options are passed as additional arguments to the ABC command
+implementing the solver.
 
 Script section
 --------------