Overview

The OneSpin IPC Verification Tool is a formal verification tool associated with Interval Property Checking (IPC). In the available evidence, IPC is described as a SAT-based formal verification methodology used to check whether a hardware design satisfies a set of properties written in a dedicated verification language. The same source states that completeness analysis integrated within an IPC verification environment was commercially available.

Verification method

IPC is presented as a technique related to Bounded Model Checking, but focused on safety properties. Instead of starting only from an initial state, IPC uses an arbitrary starting state; if a property holds from an arbitrary state, it also holds from any reachable state, giving exhaustive verification for that property. The evidence also notes that false negatives can occur when counterexamples originate from unreachable states, and that invariants may be added to restrict the starting state.

The properties in the cited work are written in ITL, a language in which temporal logic expressions describe the behavior of a synchronous sequential system, with discrete time steps corresponding to clock cycles.

Completeness analysis

The tool environment is associated with completeness analysis. In the cited methodology, completeness analysis determines whether every possible input scenario, corresponding to a design transaction sequence, can be covered by a chain of properties that predicts states and outputs at every point in time. The source states that any two designs satisfying all properties of a complete property suite are formally equivalent.

The completeness check is described as ensuring, at the end state of each property, that:

• there is always a successor property with matching assumptions;
• the successor property is uniquely determined; and
• each property uniquely describes the outputs and states of the design under verification.

Use in ISS generation research

The paper Generating an Efficient Instruction Set Simulator from a Complete Property Suite uses IPC and completeness analysis in the context of deriving an instruction set simulator (ISS) from a complete property suite. The paper argues that an ISS derived from the ISA used for formal verification can avoid discrepancies between the simulator and the hardware design. It reports that a processor property suite and its completeness were successfully checked against the processor design using the referenced commercial IPC environment, making the property suite a correct and complete specification for the purposes of the experiment.

The same work reports generated simulator performance of 7.0 MIPS for a simple processor design and 1.2 MIPS for an industrial design, compared with 14.0 MIPS and 2.5 MIPS respectively for custom just-in-time compiled simulators. The authors characterize the generated ISS performance as comparable to modern custom instruction-set simulators, while noting that custom JIT simulators remained faster because of tool optimizations and because properties may include hardware and pipeline effects not present in a high-level ISA description.