Add ITP engine: interpolation-based model checking via itp-bmc

docs/source/reference.rst

@@ -446,6 +446,67 @@ Example:
    [engines]
    abc --keep-going pdr
 
+``itp`` engine
+~~~~~~~~~~~~~~
+
+The ``itp`` engine implements interpolation-based model checking using Craig
+interpolants extracted from SAT resolution proofs. It uses the external
+`itp-bmc <https://github.com/inquisitour/itp-bmc>`_ tool.
+
+Supported modes: ``prove``, ``bmc``
+
+**Installation:**
+
+Install the ``itp-bmc`` binary to PATH:
+
+.. code-block:: bash
+
+   git clone https://github.com/inquisitour/itp-bmc.git
+   cd itp-bmc
+   make
+   sudo cp bmc /usr/local/bin/itp-bmc
+
+Or set the ``ITP_BMC`` environment variable to point to the binary.
+
+**Engine arguments:**
+
+.. code-block:: sby
+
+   [engines]
+   itp <bound> <skip>
+
++------------+--------------------------------------------------------------+
+|  Argument  | Description                                                  |
++============+==============================================================+
+| ``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                       |
++------------+--------------------------------------------------------------+
+
+**Example:**
+
+.. code-block:: sby
+
+   [options]
+   mode prove
+
+   [engines]
+   itp 20 0
+
+For designs requiring reset cycles (e.g. riscv-formal):
+
+.. code-block:: sby
+
+   [engines]
+   itp 15 10
+
+.. note::
+
+   The ``itp`` engine does not currently produce counterexample witness
+   traces. When a property violation is found, only FAIL status is reported.
+
 ``none`` engine
 ~~~~~~~~~~~~~~~
 

sbysrc/sby_engine_itp.py

@@ -0,0 +1,137 @@
+#
+# SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
+# ITP engine: interpolation-based model checking using Craig interpolants
+#
+# Contributor:  Pratik Deshmukh <deshmukhpratik931@gmail.com>
+#
+# Permission to use, copy, modify, and/or distribute this software for any
+# purpose with or without fee is hereby granted, provided that the above
+# copyright notice and this permission notice appear in all copies.
+#
+# THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+# WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+# MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+# ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+# WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+# ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+#
+# Usage in .sby file:
+#   [engines]
+#   itp [bound] [skip]
+#
+#   bound: maximum unrolling depth (default: task opt_depth or 20)
+#   skip:  number of initial timeframes to skip before checking bad states
+#          (default: task opt_skip or 0)
+#
+# The engine uses the 'itp-bmc' binary which must be either:
+#   1. Available in PATH as 'itp-bmc'
+#   2. Specified via the ITP_BMC environment variable
+#
+# Note: This engine currently does not produce counterexample witness traces.
+# When a property violation is found (FAIL), no .aiw or .yw trace file is
+# generated. Trace generation support is planned for a future version.
+#
+
+import os, getopt, shutil
+from sby_core import SbyProc
+
+def find_itp_bmc(task, engine_idx):
+    """Locate the itp-bmc binary via ITP_BMC env var or PATH."""
+    if "ITP_BMC" in os.environ:
+        path = os.environ["ITP_BMC"]
+        if not os.path.isfile(path):
+            task.error(f"engine_{engine_idx}: ITP_BMC set to '{path}' but file not found.")
+        return path
+    found = shutil.which("itp-bmc")
+    if found:
+        return found
+    task.error(
+        f"engine_{engine_idx}: 'itp-bmc' not found. "
+        f"Install it to PATH or set the ITP_BMC environment variable."
+    )
+
+def run(mode, task, engine_idx, engine):
+    if mode not in ["prove", "bmc"]:
+        task.error(f"engine_{engine_idx}: The itp engine is only supported in prove and bmc modes.")
+
+    # Parse options
+    opts, args = getopt.getopt(engine[1:], "", ["depth=", "skip="])
+
+    # Defaults from task options
+    bound = getattr(task, "opt_depth", 20) or 20
+    skip  = getattr(task, "opt_skip",  0)  or 0
+
+    for o, a in opts:
+        if o == "--depth":
+            bound = int(a)
+        elif o == "--skip":
+            skip = int(a)
+        else:
+            task.error(f"engine_{engine_idx}: Invalid itp option '{o}'.")
+
+    # Positional args override: itp [bound] [skip]
+    if len(args) > 0:
+        try:
+            bound = int(args[0])
+        except ValueError:
+            task.error(f"engine_{engine_idx}: Invalid bound value '{args[0]}', expected integer.")
+    if len(args) > 1:
+        try:
+            skip = int(args[1])
+        except ValueError:
+            task.error(f"engine_{engine_idx}: Invalid skip value '{args[1]}', expected integer.")
+    if len(args) > 2:
+        task.error(f"engine_{engine_idx}: Too many arguments to itp 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)
+    bmc_binary  = find_itp_bmc(task, engine_idx)
+    bmc_workdir = os.path.dirname(os.path.realpath(bmc_binary))
+
+    log = task.log_prefix(f"engine_{engine_idx}")
+
+    # Input: binary AIGER model generated by sby
+    aig_src = f"{task.workdir}/model/design_aiger.aig"
+
+    log(f"Running interpolation-based model checker: bound={bound}, skip={skip}")
+
+    proc_status = None
+
+    def output_callback(line):
+        nonlocal proc_status
+        if "Fixpoint reached" in line:
+            log("Interpolation fixpoint reached — property proved SAFE")
+        elif "Counterexample found" in line:
+            log("Counterexample found — property UNSAFE")
+            proc_status = "FAIL"
+        elif "Safe up to bound" in line:
+            log(f"Bounded safety result (fixpoint not reached): {line.strip()}")
+        return line
+
+    def exit_callback(retcode):
+        nonlocal proc_status
+        if retcode == 0:
+            proc_status = "PASS"
+        else:
+            proc_status = "FAIL"
+
+        if proc_status is None:
+            task.error(f"engine_{engine_idx}: Engine terminated without producing a status.")
+
+        task.update_status(proc_status)
+        task.summary.set_engine_status(engine_idx, proc_status)
+        task.terminate()
+
+    proc = SbyProc(
+        task,
+        f"engine_{engine_idx}",
+        task.model("aig"),
+        f"BMC_WORKDIR={bmc_workdir} {bmc_binary} {bound} {aig_src} {skip}",
+        logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w"),
+    )
+
+    proc.output_callback = output_callback
+    proc.register_exit_callback(exit_callback)

sbysrc/sby_mode_bmc.py

@@ -43,6 +43,10 @@ def run(task):
             import sby_engine_btor
             sby_engine_btor.run("bmc", task, engine_idx, engine)
 
+        elif engine[0] == "itp":
+            import sby_engine_itp
+            sby_engine_itp.run("bmc", task, engine_idx, engine)
+
         elif engine[0] == "none":
             pass
 

sbysrc/sby_mode_prove.py

@@ -46,6 +46,10 @@ def run(task):
             import sby_engine_abc
             sby_engine_abc.run("prove", task, engine_idx, engine)
 
+        elif engine[0] == "itp":
+            import sby_engine_itp
+            sby_engine_itp.run("prove", task, engine_idx, engine)
+
         elif engine[0] == "none":
             pass