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

itp engine: add skip and fixpoint justification

Browse source
This commit is contained in:
inquisitour 2026-05-15 05:19:58 +00:00
parent b32d0e63c3
commit b01f30d763
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
docs/source/reference.rst
View file

@ -514,7 +514,9 @@ The ``itp`` engine has been verified to produce unbounded safety proofs
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.
results only, as pure BMC cannot rule out paths through invalid reset
states without inductive reasoning. This is a property of BMC-based
interpolation, not a limitation specific to this engine.
The ``itp`` engine does not currently produce counterexample witness
traces. When a property violation is found, only FAIL status is reported.