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

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

Browse source
This commit is contained in:
N. Engelhardt 2022-03-25 18:01:09 +01:00
parent fa5d5ad831
commit 3834fe7622
1 changed files with 52 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

54
docs/source/reference.rst
View file

@ -120,10 +120,12 @@ Mode Description
``prove`` Unbounded model check to verify safety properties (``assert(...)`` statements) ``prove`` Unbounded model check to verify safety properties (``assert(...)`` statements)
``live`` Unbounded model check to verify liveness properties (``assert(s_eventually ...)`` 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 ``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 All other options have default values and thus are optional. The available
options are: options are:
@ -197,6 +199,38 @@ solver options.
In the 2nd line ``abc`` is the engine, there are no engine options, ``sim3`` is the In the 2nd line ``abc`` is the engine, there are no engine options, ``sim3`` is the
solver, and ``-W 15`` are solver options. 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 ``smtbmc`` engine
~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~
@ -240,12 +274,28 @@ The following solvers are currently supported by ``yosys-smtbmc``:
* yices * yices
* boolector * boolector
* bitwuzla
* z3 * z3
* mathsat * mathsat
* cvc4 * cvc4
Any additional options after ``--`` are passed to ``yosys-smtbmc`` as-is. 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 ``aiger`` engine
~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~