mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 22:14:08 +00:00
Code Activity

Add engines documentation

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-03 15:54:00 +01:00
parent 236f6412c1
commit 23a369e16d
1 changed files with 104 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

105
docs/source/reference.rst
View file

@ -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
--------------