DocumentCode
3391715
Title
Reverification of a microprocessor
Author
Crocker, S.D. ; Cohen, Eve ; Landauer, Sue ; Orman, Hilarie
Author_Institution
Trusted Inf. Syst., Los Angeles, CA, USA
fYear
1988
fDate
18-21 Apr 1988
Firstpage
166
Lastpage
176
Abstract
The FM8501 microprocessor was defined and verified by W.A. Hunt (1986) using the Boyer-Moore theorem-prover. The authors have carried out a reverification of the machine using the State Delta Verification System. Their work correlates strongly with work done by Hunt, demonstrating that the verification community is capable of supporting its own results, drawing on the diversification of proof tools to provide independent validation of previous work. The proof strategies and the complexities that are encountered in proving correctness of microcoded processors are discussed
Keywords
computer testing; microprocessor chips; program verification; security of data; theorem proving; Boyer-Moore theorem-prover; FM8501; State Delta Verification System; complexities; correctness; microcoded processors; microprocessor; proof strategies; verification community; Arithmetic; Hardware; Information systems; Logic; Microprocessors; Paper making machines; Programming profession; Registers; Writing;
fLanguage
English
Publisher
ieee
Conference_Titel
Security and Privacy, 1988. Proceedings., 1988 IEEE Symposium on
Conference_Location
Oakland, CA
Print_ISBN
0-8186-0850-1
Type
conf
DOI
10.1109/SECPRI.1988.8109
Filename
8109
Link To Document