mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-06-08 14:20:59 +00:00
Code Activity

Merge pull request #351 from Goubermouche/main

Browse source 
Document abc --keep-going pdr [sc-220]
This commit is contained in:
KrystalDelusion 2026-02-24 09:28:45 +13:00 • committed by GitHub
commit 4dabe8ab32
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 21 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

24
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. 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 | | ``--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. |
@ -411,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 The ``abc`` engine is a front-end for the functionality in Berkeley ABC. It
currently supports no engine options and supports the following supports the following solvers:
solvers:
+------------+-----------------+---------------------------------+ +------------+-----------------+---------------------------------+
| Solver | Modes | ABC Command | | Solver | Modes | ABC Command |
@ -427,6 +428,23 @@ 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 (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, rather than a |
| | single global result. |
+------------------+---------------------------------------------------------+
Example:
.. code-block:: sby
[engines]
abc --keep-going pdr
``none`` engine ``none`` engine
~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~