Skip to content
STIMSMITH

Interval Property Checking

Technique

Interval Property Checking (IPC) is a SAT-based formal verification technique for synchronous digital circuits that verifies safety properties over bounded intervals from arbitrary starting states. Unlike original bounded model checking, IPC is described as using arbitrary rather than initial states, so a property that holds from any arbitrary state also holds from any reachable state; unreachable-state counterexamples can occur and are handled by adding invariants.

First seen 5/26/2026
Last seen 6/8/2026
Evidence 9 chunks
Wiki v1

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

18 connections
Finite State Machine uses → 100% 3e
IPC models synchronous circuits as finite state machines.
Bounded Model Checking extends → 90% 3e
IPC is described as a technique similar to but extending Bounded Model Checking.
Boolean Satisfiability uses → 100% 3e
IPC uses SAT-based methods for verification.
Generating an Efficient Instruction Set Simulator from a Complete Property Suite ← uses 100% 2e
The paper uses Interval Property Checking as the formal verification technique.
Completeness Analysis ← part of 90% 2e
Completeness analysis is integrated within the IPC verification environment.
Processor Verification ← uses 95% 2e
Processor verification is carried out using interval property checking methodology.
OneSpin 360 MV ← implements 95% 2e
OneSpin 360 MV implements Interval Property Checking as its verification engine.
SAT-based Formal Verification uses → 90% 2e
IPC uses SAT solving to find counterexamples.
Safety Properties uses → 95% 2e
IPC verifies only safety properties.
Invariant Generation uses → 90% 2e
IPC uses invariants to avoid unreachable counterexamples, and these can be automatically generated.
Advanced Automation in Formal Verification of Processors ← uses 95% 2e
The paper uses IPC as the core verification technique.
Safety Property evaluates → 100% 1e
IPC is restricted to verifying safety properties of digital circuits.
ITL uses → 100% 1e
ITL is the language used to express properties in interval property checking.
Completeness Analysis uses → 100% 1e
IPC uses completeness analysis to determine whether the property suite covers all behaviors.
OneSpin IPC Verification Tool ← implements 95% 1e
The OneSpin tool is a commercial IPC verification environment.
Bounded Model Checking uses → 95% 1e
Interval Property Checking is a variant of Bounded Model Checking used for safety property verification.
Safety Property uses → 100% 1e
IPC only verifies safety properties.
Invariant uses → 100% 1e
IPC uses invariants to restrict the starting state and remove false negatives.

LINKED ENTITIES

2 links
Bounded Model Checking contrasted_with The evidence explicitly contrasts IPC with original BMC, stating that IPC uses an arbitrary starting state instead of the initial state used in BMC.
Boolean Satisfiability uses The evidence states that IPC produces bounded properties that can be checked efficiently using a SAT solver and gives a SAT instance used to search for counterexamples.

CITATIONS

10 sources
10 citations — click to expand
[1] IPC as methodology Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[2] BMC and SAT context Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[3] IPC verifies safety properties efficiently using SAT Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[4] IPC arbitrary starting state Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[5] False negatives and invariants Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[6] FSM and safety-property formalization Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[7] IPC SAT instance Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[8] Completeness analysis criteria Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[9] ITL property language Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[10] Complete property suite as model Generating an Efficient Instruction Set Simulator from a Complete Property Suite