From 23a369e16df80ca624ae5d4ee252726172f631f9 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 3 Mar 2018 15:54:00 +0100 Subject: [PATCH] Add engines documentation Signed-off-by: Clifford Wolf --- docs/source/reference.rst | 105 +++++++++++++++++++++++++++++++++++++- 1 file changed, 104 insertions(+), 1 deletion(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 7a48112..c8951e5 100644 --- 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 -v`` | ++------------+-----------------+---------------------------------+ +| ``sim3`` | ``bmc`` | ``sim3 -F -v`` | ++------------+-----------------+---------------------------------+ +| ``pdr`` | ``prove`` | ``pdr`` | ++------------+-----------------+---------------------------------+ + +Solver options are passed as additional arguments to the ABC command +implementing the solver. Script section -------------- -- 2.30.2