Zurab Khasidashvili (Intel Haifa) 

"Verifying Equivalence of Memories Using a First Order Logic Theorem Prover"
   
Abstract:

We propose a new method of equivalence checking of RTL and schematic
descriptions of memories using translation in first-order logic. Our
method is based on a powerful abstraction of memories and address
decoders in them. We propose two ways of axiomatizing decoders and
memories. The first axiomatization uses 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 decidable fragment of
first-order logic. Equivalence of real-life memories cam be verified
in seconds with our approach.

Joint work with Andrei Voronkov and Mahmoud Kinanah