Patent ID: 7836414

Claim:
A method for formally proving the functional equivalence of pipelined designs containing memories, comprising: receiving a specification for a first pipelined design and a specification for a second pipelined design, wherein the first pipelined design includes a first memory system and the second pipelined design includes a second memory system; generating, using one or more computers, representations of the first pipelined design and the second pipelined design in a combinational form, wherein the representations are generated based partly or solely on a correspondence between memory operations on the first memory system and corresponding memory operations on the second memory system, and wherein memory operations in the first memory system and the second memory system are converted into corresponding combinational operations based partly or solely on design inputs; and comparing the combinational outputs of the first pipelined design and the combinational outputs of the second pipelined design to verify that the first pipelined design and the second pipelined design are functionally equivalent.