From 39670d661133065a46d1949cc47b07567ba73217 Mon Sep 17 00:00:00 2001 From: inquisitour Date: Sat, 28 Feb 2026 07:11:08 +0000 Subject: [PATCH] Add ITP engine: interpolation-based model checking via itp-bmc --- docs/source/reference.rst | 61 +++++++++++++++++ sbysrc/sby_engine_itp.py | 137 ++++++++++++++++++++++++++++++++++++++ sbysrc/sby_mode_bmc.py | 4 ++ sbysrc/sby_mode_prove.py | 4 ++ 4 files changed, 206 insertions(+) create mode 100644 sbysrc/sby_engine_itp.py diff --git a/docs/source/reference.rst b/docs/source/reference.rst index d322d65..716716e 100644 --- a/docs/source/reference.rst +++ b/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 `_ 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 + ++------------+--------------------------------------------------------------+ +| 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 ~~~~~~~~~~~~~~~ diff --git a/sbysrc/sby_engine_itp.py b/sbysrc/sby_engine_itp.py new file mode 100644 index 0000000..2d732eb --- /dev/null +++ b/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 +# +# 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) \ No newline at end of file diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index 173812f..34de5e0 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/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 diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index e50fbfd..c608c6b 100644 --- a/sbysrc/sby_mode_prove.py +++ b/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