Formal specification and verification techniques for RISC pipeline conflicts

We outline a general methodology for the formal verification of instruction pipelines in RISC cores. The different kinds of conflicts, i. e. resource, data and control conflicts that can occur due to the simultaneous execution of the instructions in the pipeline, have been formally specified in higher order logic. Based on a hierarchical model for RISC processors, we have developed a constructive proof methodology, i.e. when conflicts at a specific abstraction level are detected, the conditions under which these occur are generated and explicitly output to the designer, thus easing their removal. All implemented specifications and tactics are kept general, so that they are usable for a wide range of RISC cores. In this paper, the described formalization and proof strategies are illustrated via the DLX RISC processor.