A Methodology for the Formal Verification of RISC Microprocessors A Functional Approach

We propose a methodological approach for the formal specification and verification of RISC processor microarchitectures within a functional framework. The approach exploits only the next state function to formally specify both ISA and MA levels and proves their equivalence in a systematic way. Moreover, the proof could be performed at different architectural levels. The central idea consists of decomposing the next state function into coordinates such that to model the microarchitecture 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.