Title :
Reverification of a microprocessor
Author :
Crocker, S.D. ; Cohen, Eve ; Landauer, Sue ; Orman, Hilarie
Author_Institution :
Trusted Inf. Syst., Los Angeles, CA, USA
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;
Conference_Titel :
Security and Privacy, 1988. Proceedings., 1988 IEEE Symposium on
Conference_Location :
Oakland, CA
Print_ISBN :
0-8186-0850-1
DOI :
10.1109/SECPRI.1988.8109
