Verifying equivalence of memories using a first order logic theorem prover

We propose a new method for equivalence checking of RTL and schematic descriptions of memories using translation into first-order logic. Our method is based on a powerful abstraction of memories and address decoders within them. We propose two ways of axiomatizing some of the bit-vector operations, decoders, and memories. The first axiomatization uses an algebra of operations on bit-vectors. The second axiomatization considers a bit-vector as a unary relation and memory as a relation of larger arity. For some designs, including real-life designs, the second axiomatization results in a first-order problem falling into a known decidable fragment of first-order logic and suitable for solving by modern first-order provers. Equivalence of real-life memories can be verified in seconds with our approach. © 2009 IEEE.