From: N. Engelhardt <nak@yosyshq.com>
Date: Fri, 25 Mar 2022 17:01:09 +0000 (+0100)
Subject: document btor engine, add overview of mode/engine/solver combinations, remove unimple... 
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3834fe76226f39b87f4104d5e908d9cb82106cdf;p=SymbiYosys.git

document btor engine, add overview of mode/engine/solver combinations, remove unimplemented modes
---

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index dc5f336..9cbf78b 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -120,10 +120,12 @@ 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
-``equiv`` Formal equivalence checking (usually to verify pre- and post-synthesis equivalence)
-``synth`` Reactive Synthesis (synthesis of circuit from safety properties)
 ========= ===========
 
+..
+   ``equiv`` Formal equivalence checking (usually to verify pre- and post-synthesis equivalence)
+   ``synth`` Reactive Synthesis (synthesis of circuit from safety properties)
+
 All other options have default values and thus are optional. The available
 options are:
 
@@ -197,6 +199,38 @@ 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 following mode/engine/solver combinations are currently supported:
+
++-----------+--------------------------+
+| Mode      | Engine                   |
++===========+==========================+
+| ``bmc``   | ``smtbmc [all solvers]`` |
+|           |                          |
+|           | ``btor btormc``          |
+|           |                          |
+|           | ``btor pono``            |
+|           |                          |
+|           | ``abc bmc3``             |
+|           |                          |
+|           | ``abc sim3``             |
++-----------+--------------------------+
+| ``prove`` | ``smtbmc [all solvers]`` |
+|           |                          |
+|           | ``abc pdr``              |
+|           |                          |
+|           | ``aiger avy``            |
+|           |                          |
+|           | ``aiger suprove``        |
++-----------+--------------------------+
+| ``cover`` | ``smtbmc [all solvers]`` |
+|           |                          |
+|           | ``btor btormc``          |
++-----------+--------------------------+
+| ``live``  | ``aiger suprove``        |
+|           |                          |
+|           | ``aiger avy``            |
++-----------+--------------------------+
+
 ``smtbmc`` engine
 ~~~~~~~~~~~~~~~~~
 
@@ -240,12 +274,28 @@ The following solvers are currently supported by ``yosys-smtbmc``:
 
   * yices
   * boolector
+  * bitwuzla
   * z3
   * mathsat
   * cvc4
 
 Any additional options after ``--`` are passed to ``yosys-smtbmc`` as-is.
 
+``btor`` engine
+~~~~~~~~~~~~~~~
+
+The ``btor`` engine supports hardware modelcheckers that accept btor2 files.
+The engine supports no engine options and supports the following solvers:
+
++-------------------------------+---------------------------------+
+|   Solver                      |   Modes                         |
++===============================+=================================+
+| ``btormc``                    |   ``bmc``, ``cover``            |
++-------------------------------+---------------------------------+
+| ``pono``                      |   ``bmc``                       |
++-------------------------------+---------------------------------+
+
+
 ``aiger`` engine
 ~~~~~~~~~~~~~~~~