mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-02-22 03:07:38 +00:00
Code Activity

Cleanup docs.

Browse source
This commit is contained in:
nella 2026-02-18 09:35:17 +01:00
parent b153c8e080
commit a6746d0b58
1 changed files with 7 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

27
docs/source/reference.rst
View file

@ -343,9 +343,9 @@ the following options:
| | warmup the SMT solver). |
+------------------+---------------------------------------------------------+
| ``--keep-going`` | In BMC mode, continue after the first failed assertion |
| | and report further failed assertions. (The ``abc`` |
| | engine also supports ``--keep-going`` with ``pdr``; see |
| | the ``abc`` engine section below.) |
| | and report further failed assertions. In prove mode, |
| | ``--keep-going`` is currently only supported with |
| | ``abc pdr`` (see the ``abc`` engine section below). |
+------------------+---------------------------------------------------------+
| ``--unroll``, | Disable/enable unrolling of the SMT problem. The |
| ``--nounroll`` | default value depends on the solver being used. |
@ -413,8 +413,7 @@ Solver options are passed to the solver as additional command line options.
~~~~~~~~~~~~~~
The ``abc`` engine is a front-end for the functionality in Berkeley ABC. It
currently supports no engine options and supports the following
solvers:
supports the following solvers:
+------------+-----------------+---------------------------------+
| Solver | Modes | ABC Command |
@ -430,27 +429,16 @@ Solver options are passed as additional arguments to the ABC command
implementing the solver.
When using the ``pdr`` solver, the ``abc`` engine supports the following
engine option:
engine option (currently the only engine option available for ``abc``):
+------------------+---------------------------------------------------------+
| Option | Description |
+==================+=========================================================+
| ``--keep-going`` | Continue after the first proven or failed assertion and |
| | report individual per-property results. When enabled, |
| | SBY uses the AIGER witness map (``write_aiger -ywmap``) |
| | to track each ``$assert`` cell individually and reports |
| | pass/fail status per property rather than a single |
| | global result. |
| | report individual per-property results, rather than a |
| | single global result. |
+------------------+---------------------------------------------------------+
.. note::
The ``--keep-going`` option for ``abc pdr`` requires a Yosys version that
includes witness-aware AIGER map output (``write_aiger -ywmap`` with
assert/assume path tracking) and the ``rename -witness`` pass covering
formal property cells. The default ``prep`` command already runs
``rename -witness``.
Example:
.. code-block:: sby
@ -458,7 +446,6 @@ Example:
[engines]
abc --keep-going pdr
``none`` engine
~~~~~~~~~~~~~~~