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

itp engine: fix BMC_WORKDIR path, update docs with 4-core benchmark results

Browse source
This commit is contained in:
inquisitour 2026-05-15 05:05:44 +00:00
parent a6a42216f5
commit b32d0e63c3
2 changed files with 21 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

26
docs/source/reference.rst
View file

@ -466,7 +466,8 @@ Install the ``itp-bmc`` binary to PATH:
make
sudo cp bmc /usr/local/bin/itp-bmc
Or set the ``ITP_BMC`` environment variable, or use the ``--itp-bmc`` command-line flag to specify the path directly.
Or set the ``ITP_BMC`` environment variable, or use the ``--itp-bmc``
command-line flag to specify the path directly.
**Engine arguments:**
@ -481,8 +482,7 @@ Or set the ``ITP_BMC`` environment variable, or use the ``--itp-bmc`` command-li
| ``bound`` | Maximum unrolling depth. Default: value of ``depth`` option |
+------------+--------------------------------------------------------------+
| ``skip`` | Number of initial timeframes to skip before checking bad |
| | states. Useful for designs requiring reset cycles. |
| | Default: value of ``skip`` option or 0 |
| | states. Default: value of ``skip`` option or 0 |
+------------+--------------------------------------------------------------+
**Example:**
@ -495,15 +495,27 @@ Or set the ``ITP_BMC`` environment variable, or use the ``--itp-bmc`` command-li
[engines]
itp 20 0
For designs requiring reset cycles (e.g. riscv-formal):
**Tested on:**
.. code-block:: sby
The ``itp`` engine has been verified to produce unbounded safety proofs
(fixpoint convergence) on the following RISC-V cores using the
`riscv-formal <https://github.com/YosysHQ/riscv-formal>`_ framework
(instructions checked: add, sub, and, or, xor, lui):
[engines]
itp 15 10
- NERV — 6/6 instruction checks, fixpoint at bound 2
- PicoRV32 — 6/6 instruction checks, fixpoint at bound 2
- SERV — 6/6 instruction checks, fixpoint at bound 2
- VexRiscv — 6/6 instruction checks, fixpoint at bound 2
.. note::
The ``itp`` engine achieves unbounded safety proofs via interpolant
fixpoint detection. The ``skip`` parameter skips bad-state checking
for the first ``skip`` timeframes, but fixpoint convergence is only
guaranteed when ``skip`` is set to 0. Designs requiring non-zero
``skip`` values (e.g. multi-cycle reset sequences) will return bounded
results only.
The ``itp`` engine does not currently produce counterexample witness
traces. When a property violation is found, only FAIL status is reported.