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

Merge a6746d0b58 into 16171682e4

Browse source
This commit is contained in:
nella 2026-02-18 08:35:25 +00:00 • committed by GitHub
commit 7a108bdfd3
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). |
+------------------+---------------------------------------------------------+
| ``--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 |
| ``--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
currently supports no engine options and supports the following
solvers:
supports the following solvers:
+------------+-----------------+---------------------------------+
| Solver | Modes | ABC Command |
@ -427,6 +428,23 @@ solvers:
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 (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
~~~~~~~~~~~~~~~