File(s) stored somewhere else

Please note: Linked content is NOT stored on Carnegie Mellon University and we can't guarantee its availability, quality, security or accept any liability.

Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation

journal contribution
posted on 01.01.1997, 00:00 authored by Randal BryantRandal 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.


Publisher Statement

All Rights Reserved