Verifying pipelined microprocessors

Author

Windley, Phillip J.

Author_Institution

Dept. of Comput. Sci., Brigham Young Univ., Provo, UT, USA

fYear

1995

fDate

29 Aug-1 Sep 1995

Firstpage

503

Lastpage

511

Abstract

Recently there has been much research in verifying pipelined microprocessors. Even so, there has been little consensus on what form the correctness statement should take. Put another way, what should we be verifying about pipelined microprocessors? We believe that the correctness statement should show that the parallel machine represented by the pipeline behaves in the same manner as the sequential machine represented by the instruction set semantics. In this paper, we present such a model and examine four pipeline verifications to see how they compare

Keywords

computer testing; formal logic; formal verification; integrated circuit testing; logic testing; microprocessor chips; pipeline processing; theorem proving; correctness statement; instruction set semantics; parallel machine; pipelined microprocessors; verifying; Computer science; Formal specifications; Formal verification; Laboratories; Logic; Microprocessors; Parallel machines; Pipelines; Robustness;

fLanguage

English

Publisher

ieee

Conference_Titel

Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL '95/VLSI '95., IFIP International Conference on Hardware Description Languages. IFIP International Conference on Very Large Scal

Conference_Location

Chiba

Print_ISBN

4-930813-67-0

Type

conf

DOI

10.1109/ASPDAC.1995.486362

Filename

486362