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

[inquisitour]

Summary

Adds a new itp engine for interpolation-based model checking using Craig interpolants.

Why ITP?

All existing sby engines that support prove mode rely on either k-induction
(smtbmc) or PDR/IC3 variants (abc pdr, avy, rIC3, suprove). The itp engine
adds a distinct proof strategy: interpolation-based reachability analysis.

Unlike BMC-only engines (aigbmc, btormc) which can only check up to a finite
bound, the itp engine achieves unbounded safety proofs by computing
Craig interpolants from SAT refutation proofs and checking for fixpoint
convergence. When the over-approximation of reachable states stabilizes, the
property is proved safe for all reachable executions — not just up to a bound.

This complements existing engines:

• On circuits where k-induction requires deep unrolling, interpolation can
  converge in just a few iterations
• Provides an alternative proof path when PDR/IC3 engines time out or fail
• Uses only a SAT solver with proof logging (MiniSAT) — no SMT solver required

Changes

• sbysrc/sby_engine_itp.py — new engine implementation
• sbysrc/sby_mode_prove.py — register itp engine in prove mode
• sbysrc/sby_mode_bmc.py — register itp engine in bmc mode
• docs/source/reference.rst — documentation for the new engine

Backend Tool

Requires itp-bmc: https://github.com/inquisitour/itp-bmc

git clone https://github.com/inquisitour/itp-bmc.git
cd itp-bmc && make
sudo cp bmc /usr/local/bin/itp-bmc

Usage

[engines]
itp <bound> <skip>

Tested On

riscv-formal NERV core: insn_add, insn_sub, insn_and, insn_or, insn_xor, insn_lui — all PASS

Limitations

• No counterexample witness traces yet (planned)
• Safety checking only (no liveness)