From 39670d661133065a46d1949cc47b07567ba73217 Mon Sep 17 00:00:00 2001 From: inquisitour Date: Sat, 28 Feb 2026 07:11:08 +0000 Subject: [PATCH 1/4] 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 From 7225ad24f1cb5e929e4d205a09ebc42ac503209d Mon Sep 17 00:00:00 2001 From: inquisitour Date: Sat, 14 Mar 2026 18:07:04 +0000 Subject: [PATCH 2/4] itp engine: address review feedback - simplify arg parsing, fix status logic, use exe_paths --- docs/source/reference.rst | 2 +- sbysrc/sby_cmdline.py | 2 ++ sbysrc/sby_core.py | 1 + sbysrc/sby_engine_itp.py | 40 ++++++++------------------------------- 4 files changed, 12 insertions(+), 33 deletions(-) diff --git a/docs/source/reference.rst b/docs/source/reference.rst index 716716e..a50e31e 100644 --- a/docs/source/reference.rst +++ b/docs/source/reference.rst @@ -466,7 +466,7 @@ Install the ``itp-bmc`` binary to PATH: make sudo cp bmc /usr/local/bin/itp-bmc -Or set the ``ITP_BMC`` environment variable to point to the binary. +Or set the ``ITP_BMC`` environment variable, or use the ``--itp-bmc`` command-line flag to specify the path directly. **Engine arguments:** diff --git a/sbysrc/sby_cmdline.py b/sbysrc/sby_cmdline.py index d7952ef..a5995f2 100644 --- a/sbysrc/sby_cmdline.py +++ b/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="", action=DictAction, dest="exe_paths") + parser.add_argument("--itp-bmc", metavar="", + action=DictAction, dest="exe_paths") parser.add_argument("--pono", metavar="", action=DictAction, dest="exe_paths", help="configure which executable to use for the respective tool") diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 7a67cd3..1ffa2c8 100644 --- a/sbysrc/sby_core.py +++ b/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() diff --git a/sbysrc/sby_engine_itp.py b/sbysrc/sby_engine_itp.py index 2d732eb..ce2e21c 100644 --- a/sbysrc/sby_engine_itp.py +++ b/sbysrc/sby_engine_itp.py @@ -33,43 +33,20 @@ # generated. Trace generation support is planned for a future version. # -import os, getopt, shutil +import os, getopt 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="]) + args = engine[1:] # 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: @@ -88,7 +65,7 @@ def run(mode, task, engine_idx, engine): 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_binary = task.exe_paths["itp-bmc"] bmc_workdir = os.path.dirname(os.path.realpath(bmc_binary)) log = task.log_prefix(f"engine_{engine_idx}") @@ -104,22 +81,21 @@ def run(mode, task, engine_idx, engine): 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") - proc_status = "FAIL" 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 retcode == 0: - proc_status = "PASS" - else: - proc_status = "FAIL" + # If output_callback already determined status (e.g. from output lines), + # trust that over the exit code if proc_status is None: - task.error(f"engine_{engine_idx}: Engine terminated without producing a status.") + proc_status = "PASS" if retcode == 0 else "FAIL" task.update_status(proc_status) task.summary.set_engine_status(engine_idx, proc_status) From 01a716bf2e973f8fc014e3879f966b03b038350b Mon Sep 17 00:00:00 2001 From: inquisitour Date: Sat, 14 Mar 2026 20:33:17 +0000 Subject: [PATCH 3/4] itp engine: address review feedback - use constants --- sbysrc/sby_engine_itp.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/sbysrc/sby_engine_itp.py b/sbysrc/sby_engine_itp.py index ce2e21c..61d201c 100644 --- a/sbysrc/sby_engine_itp.py +++ b/sbysrc/sby_engine_itp.py @@ -43,9 +43,12 @@ def run(mode, task, engine_idx, engine): # Parse options args = engine[1:] + DEFAULT_BOUND = 20 + DEFAULT_SKIP = 0 + # Defaults from task options - bound = getattr(task, "opt_depth", 20) or 20 - skip = getattr(task, "opt_skip", 0) or 0 + bound = getattr(task, "opt_depth", DEFAULT_BOUND) or DEFAULT_BOUND + skip = getattr(task, "opt_skip", DEFAULT_SKIP) or DEFAULT_SKIP # Positional args override: itp [bound] [skip] if len(args) > 0: From a6a42216f5b1ab763f6f136ba6a5a0550470461c Mon Sep 17 00:00:00 2001 From: inquisitour Date: Sun, 15 Mar 2026 23:44:26 +0000 Subject: [PATCH 4/4] itp engine: use task.opt_depth and task.opt_skip directly --- sbysrc/sby_engine_itp.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/sbysrc/sby_engine_itp.py b/sbysrc/sby_engine_itp.py index 61d201c..865c45b 100644 --- a/sbysrc/sby_engine_itp.py +++ b/sbysrc/sby_engine_itp.py @@ -43,12 +43,9 @@ def run(mode, task, engine_idx, engine): # Parse options args = engine[1:] - DEFAULT_BOUND = 20 - DEFAULT_SKIP = 0 - # Defaults from task options - bound = getattr(task, "opt_depth", DEFAULT_BOUND) or DEFAULT_BOUND - skip = getattr(task, "opt_skip", DEFAULT_SKIP) or DEFAULT_SKIP + bound = task.opt_depth + skip = task.opt_skip # Positional args override: itp [bound] [skip] if len(args) > 0: