From b32d0e63c387f57ecd38a77f897944aa72ed6c4e Mon Sep 17 00:00:00 2001
From: inquisitour <deshmukhpratik931@gmail.com>
Date: Fri, 15 May 2026 05:05:44 +0000
Subject: [PATCH] itp engine: fix BMC_WORKDIR path, update docs with 4-core
 benchmark results

---
 docs/source/reference.rst | 26 +++++++++++++++++++-------
 sbysrc/sby_engine_itp.py  |  4 ++--
 2 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index a50e31e..e08b0fe 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -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.
 
diff --git a/sbysrc/sby_engine_itp.py b/sbysrc/sby_engine_itp.py
index 865c45b..d672b53 100644
--- a/sbysrc/sby_engine_itp.py
+++ b/sbysrc/sby_engine_itp.py
@@ -64,9 +64,9 @@ def run(mode, task, engine_idx, engine):
     if skip >= bound:
         task.error(f"engine_{engine_idx}: skip ({skip}) must be less than bound ({bound}).")
 
-    # Locate binary and derive workdir (for minisat relative path)
+    # Locate binary and derive workdir
     bmc_binary = task.exe_paths["itp-bmc"]
-    bmc_workdir = os.path.dirname(os.path.realpath(bmc_binary))
+    bmc_workdir = os.path.abspath(f"{task.workdir}/engine_{engine_idx}")
 
     log = task.log_prefix(f"engine_{engine_idx}")