Overview
Interval Property Checking (IPC) is a formal verification methodology used for digital circuit verification. It is presented as a SAT-based technique related to bounded model checking, but focused on verifying safety properties over bounded time intervals. The source describes IPC as the verification methodology used in the cited work and as a technique whose restrictions to safety properties lead to bounded properties that can be checked efficiently using a SAT solver.[1][2]
Relationship to bounded model checking
IPC is contrasted with the original form of Bounded Model Checking (BMC). While BMC is described as a SAT-based technique for formal verification, IPC differs by using an arbitrary starting state rather than the initial state used in BMC.[3][4]
The key implication is that if a property holds starting from an arbitrary state, then it also holds from any reachable state; in that case, the property is exhaustively verified.[4]
Property class
IPC verifies only safety properties. The source states that this is not a serious practical restriction for digital circuits because such circuits always have a finite response time, and because intended design behavior can naturally be formalized as safety properties.[2]
A safety property is given in the form f = AG(ϕ) and can be translated into a Boolean function [[f]]t that checks the validity of ϕ at a time point t. The translation is arranged so that a satisfying assignment of [[f]]t corresponds to a counterexample of ϕ.[5]
Circuit model and SAT instance
The formalization models a synchronous circuit as a finite state machine M = (I, S, S0, Δ, Λ, O), with an input alphabet, output alphabet, finite set of states, initial states, output function, and next-state function.[5]
The transition relation is given by:
T(s, s') = ∃x ∈ B^n : s' ≡ Δ(x, s)
IPC searches for counterexamples by solving a SAT instance that unrolls the transition relation over a bounded interval and connects that unrolling to a single instantiation of the translated property formula at time t.[6]
Handling false negatives
Because IPC starts from arbitrary states, it can generate false negatives: counterexamples that start in unreachable states. The source states that these false negatives must be removed by adding invariants that restrict the starting state.[7]
Completeness analysis
IPC is discussed alongside completeness analysis for property suites. Completeness analysis determines whether every possible input scenario, corresponding to a transaction sequence of the design, can be covered by a chain of properties that predicts states and outputs at every point in time.[8]
The source states that any two designs satisfying all properties of a complete property suite are formally equivalent. It also states that completeness checking reduces to checking, at the end state of each property, whether there is always a successor property with matching assumptions, whether the successor property is uniquely determined, and whether each property uniquely describes the design-under-verification states and outputs.[8]
Use with ITL properties
The cited work writes the properties in the ITL language. ITL uses temporal logic expressions to describe synchronous sequential system behavior, with discrete time steps corresponding to clock cycles. Typical ITL properties have an implication structure: if expressions in the assume part evaluate to true, expressions in the prove part must hold.[9]
ITL also supports freeze variables fixed to a time point, temporal operators such as next and prev, macro functions for abstraction, and data types of the respective HDL, including arrays and user-defined VHDL record types.[9]
Application context
The source describes IPC as powerful enough to support complete verification even for industrial designs when combined with the other techniques presented. If verification succeeds, the property suite can form a model of the verified design: the properties describe transitions and output behavior uniquely.[10]
[1]: See citation “IPC as methodology”. [2]: See citation “IPC verifies safety properties efficiently using SAT”. [3]: See citation “BMC and SAT context”. [4]: See citation “IPC arbitrary starting state”. [5]: See citation “FSM and safety-property formalization”. [6]: See citation “IPC SAT instance”. [7]: See citation “False negatives and invariants”. [8]: See citation “Completeness analysis criteria”. [9]: See citation “ITL property language”. [10]: See citation “Complete property suite as model”.