From b153c8e0803f68d7b1bd97674fb017d4a94888e1 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 11 Feb 2026 11:33:10 +0100 Subject: [PATCH 1/2] document abc --keep-going pdr [sc-220] --- docs/source/reference.rst | 33 ++++++++++++++++++++++++++++++++- 1 file changed, 32 insertions(+), 1 deletion(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index d99c2e1..2606c37 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -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. (The ``abc`` | +| | engine also supports ``--keep-going`` with ``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. | @@ -427,6 +429,35 @@ 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: + ++------------------+---------------------------------------------------------+ +| 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 ~~~~~~~~~~~~~~~ From a6746d0b583fee78df31a2b47c9f8a8d1515d311 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 18 Feb 2026 09:35:17 +0100 Subject: [PATCH 2/2] Cleanup docs. --- docs/source/reference.rst | 27 +++++++-------------------- 1 file changed, 7 insertions(+), 20 deletions(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 2606c37..d322d65 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -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 ~~~~~~~~~~~~~~~