A Scalable Proof Methodology for RISC Processor Designs: A Functional Approach

Most proof approaches verified a Pipelined Micro- Architectural implementation against an ISA specification, and consequently, it was impossible to find a meaningful point where the implementation state and the specification state can be compared easily. An alternative solution to such problem is to verify a PMA implementation against a sequential multi-cycle implementation. Because both models are formalised in terms of clock cycles, all synchronous intermediate states represent interesting points where the comparison could be achieved easily. Furthermore, by decomposing the state, the overall proof decomposes systematically into a set of verification conditions more simple to reason about and to verify. A major advantage of this elegant choice is the ability to carry out the proof by induction within the same specification language rather than by symbolic simulation through a proof tool which remains very tedious. Also, because both models relate to the MA level, there is no need for a data abstraction function (which remains very difficult to define for most approaches), only a time abstraction function is needed to map between the times used by the two models. The potential features of the proposed proof methodology are demonstrated over the pipelined MIPS RISC processor within Haskell framework.