posted on 1998-01-01, 00:00authored byRandal E. Bryant, Miroslav N Velev
This paper extends Burch and Dill’s pipeline verification method [4] to the bit level.
We introduce the idea of memory shadowing, a new technique for providing on-the-fly identical
initial memory state to two different memory execution sequences. We also present an algorithm
which compares the final states of two memories for equality. Memory shadowing and the comparison
algorithm build on the Efficient Memory Model (EMM) [13], a behavioral memory
model where the number of symbolic variables used to characterize the initial state of a memory
is proportional to the number of distinct symbolic locations accessed. These techniques allow us
to verify that a pipelined circuit has equivalent behavior to its unpipelined specification by simulating
two memory execution sequences and comparing their final states. Experimental results
show the potential of the new ideas.