Title :
Verifying pipelined microprocessors
Author :
Windley, Phillip J.
Author_Institution :
Dept. of Comput. Sci., Brigham Young Univ., Provo, UT, USA
fDate :
29 Aug-1 Sep 1995
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;
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
DOI :
10.1109/ASPDAC.1995.486362
