Patent ID: 8473883

Claim:
A method, in a data processing system, for array abstraction in an electronic design model, the method comprising: receiving, in the data processing system, an original design model having at least one memory array, wherein a correctness property of the original design model depends on an unbounded output of the at least one memory array; determining, by the data processing system, a reduced size for an abstracted memory array such that correctness of an abstracted design model comprising the abstracted memory array implies correctness of the original design model; building, by the data processing system, the abstracted design model using the reduced size for the abstracted memory array, wherein building the abstracted design model using the reduced size for the abstracted memory array comprises replacing each signal in the original design model with a composite signal having a value that represents a value of the signal in the original design model and a defined bit that represents a value that is out of range and replacing each memory array with a reduced array, wherein each element of the reduced array comprises a value that represents a value of the signal in the original design model, a defined bit that represents a value that is out of range, and an address that is modeled by the reduced array; and verifying, by the data processing system, correctness of the abstracted design model by model checking.