Patent ID: 7386818

Claim:
A computer implemented method of modeling an electronic design having one or more embedded memories, such that some or all of the memory bits comprising the one or more embedded memories need not be explicitly modeled, the method comprising the steps of: removing, one or more of the memories from the design while retaining data forwarding semantics of a memory read operation; capturing, the data forwarding semantics and memory preservation constraints for preserving an arbitrary initial memory state as Efficient Memory Modeling (EMM) constraints in a suitable representation wherein said EMM is a memory modeling technique where memory semantics is maintained without using an explicit register array model and said EMM constraints do not create structure where intermediate variables do not fan-out and do not create unnecessary 2-literal clauses; and verifying, the design using a suitable bounded analysis; and generating an output indicative of the verification wherein according to the data forwarding semantics, a memory read operation from a memory address returns a data value that was last written at that same memory address in a previous memory write operation or, if there is no previous write operation at that address then the memory read operation returns the initial data value.