mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-04-29 01:13:38 +00:00
Code Activity

document abc --keep-going pdr [sc-220]

Browse source
This commit is contained in:
nella 2026-02-11 11:33:10 +01:00
parent 16171682e4
commit b153c8e080
1 changed files with 32 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

33
docs/source/reference.rst
View file

@ -343,7 +343,9 @@ the following options:
| | warmup the SMT solver). | | | warmup the SMT solver). |
+------------------+---------------------------------------------------------+ +------------------+---------------------------------------------------------+
| ``--keep-going`` | In BMC mode, continue after the first failed assertion | | ``--keep-going`` | In BMC mode, continue after the first failed assertion |
| | and report further failed assertions. | | | and report further failed assertions. (The ``abc`` |
| | engine also supports ``--keep-going`` with ``pdr``; see |
| | the ``abc`` engine section below.) |
+------------------+---------------------------------------------------------+ +------------------+---------------------------------------------------------+
| ``--unroll``, | Disable/enable unrolling of the SMT problem. The | | ``--unroll``, | Disable/enable unrolling of the SMT problem. The |
| ``--nounroll`` | default value depends on the solver being used. | | ``--nounroll`` | default value depends on the solver being used. |
@ -427,6 +429,35 @@ solvers:
Solver options are passed as additional arguments to the ABC command Solver options are passed as additional arguments to the ABC command
implementing the solver. implementing the solver.
When using the ``pdr`` solver, the ``abc`` engine supports the following
engine option:
+------------------+---------------------------------------------------------+
| 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. |
+------------------+---------------------------------------------------------+
.. 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
[engines]
abc --keep-going pdr
``none`` engine ``none`` engine
~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~