Issue No. 04 - July/August (2003 vol. 20)
Ravi Hosabettu , Sun Microsystems
Ganesh Gopalakrishnan , University of Utah
Mandayam Srivas , Media Lab Asia
<p><div><em>Editor's note: </em></div>Complete formal verification has thus far never been achieved for a state-of-the-art, high-performance commercial microprocessor. However, this article presents a completion functions methodology, based on theorem proving, that has been applied successfully to a large variety of example pipelined architectures.<div><em>—?Carl Pixley, Synopsys</em></div></p>
R. Hosabettu, M. Srivas and G. Gopalakrishnan, "A Practical Methodology for Verifying Pipelined Microarchitectures," in IEEE Design & Test of Computers, vol. 20, no. , pp. 4-14, 2003.