Single-Threaded Formal Processor Models: Enabling Proof and High-Speed Execution

Formal veriication can be integrated into conventional computer system development by reasoning directly about system simula-tors. However, such simulators must be extremely fast to be usable in a real development eeort. We have developed a methodology for the construction of single-threaded processor models that support both formal analysis and eecient execution. This approach can, in principle, be used with any theorem prover. We describe an instantiation of our approach for models written in the logic of ACL2, and demonstrate its scalability by constructing an executable formal model of the Rockwell JEM1 Java microprocessor. We connrm that this model is single-threaded using a tool we have developed. This check permits the safe use of destructive state update optimizations that bring the performance level of the compiled formal model to that of a conventional simulator written in C.