Formal Specification and Verification of Processor Micro-Architectures Functional Approach.

This paper presents a methodological approach for the formal specification and verification of RISC processor micro-architectures within a functional framework The approach exploits only the next state function to formally specify both the Instruction-Set-Architecture (ISA) and the Micro-Architecture (MA) levels and proves their equivalence in a systematic way. The central idea consists of decomposing the next state function into coordinates such that to model the micro-architecture at the component level. Such decomposition allows the proof to be systematically decomposed into a set of verification conditions more simple to reason about and to verify, The potential features of the proof methodology are demonstrated over the MIPS processor within Haskell framework. [ABSTRACT FROM AUTHOR]