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 micro-architectures within a functional framework. The approach exploits only the next state function to formally specify both ISA and AM 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 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.