Merge a6a42216f5 into ab5bf1c10b

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, or use the ``--itp-bmc`` command-line flag to specify the path directly.
+
+**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_cmdline.py

@@ -55,6 +55,8 @@ def parser_func(release_version='unknown SBY version'):
             action=DictAction, dest="exe_paths")
     parser.add_argument("--btormc", metavar="<path_to_executable>",
             action=DictAction, dest="exe_paths")
+    parser.add_argument("--itp-bmc", metavar="<path_to_executable>",
+            action=DictAction, dest="exe_paths")
     parser.add_argument("--pono", metavar="<path_to_executable>",
             action=DictAction, dest="exe_paths",
             help="configure which executable to use for the respective tool")

sbysrc/sby_core.py

@@ -940,6 +940,7 @@ class SbyTask(SbyConfig):
             "btormc": os.getenv("BTORMC", "btormc"),
             "pono": os.getenv("PONO", "pono"),
             "imctk-eqy-engine": os.getenv("IMCTK_EQY_ENGINE", "imctk-eqy-engine"),
+            "itp-bmc": os.getenv("ITP_BMC", "itp-bmc"),
         }
 
         self.taskloop = taskloop or SbyTaskloop()

sbysrc/sby_engine_itp.py

@@ -0,0 +1,113 @@
+#
+# 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
+from sby_core import SbyProc
+
+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
+    args = engine[1:]
+
+    # Defaults from task options
+    bound = task.opt_depth
+    skip  = task.opt_skip
+
+    # 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 = task.exe_paths["itp-bmc"]
+    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")
+            proc_status = "PASS"
+        elif "Counterexample found" in line:
+            log("Counterexample found — property UNSAFE")
+        elif "Safe up to bound" in line:
+            log(f"Bounded safety result (fixpoint not reached): {line.strip()}")
+            proc_status = "PASS"
+        return line
+
+    def exit_callback(retcode):
+        nonlocal proc_status
+
+        # If output_callback already determined status (e.g. from output lines),
+        # trust that over the exit code
+        if proc_status is None:
+            proc_status = "PASS" if retcode == 0 else "FAIL"
+
+        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