Formal verification of pipeline conflicts in RISC processors

We outline a general methodology for the formal verification of pipeline conflicts in RISC cores. The different kinds of conflicts that can occur due to the simultaneous execution of the instructions in the pipeline have been formalized and automated proof techniques for each kind of conflict have been given. When conflicts are detected during the proof process, the conditions under which these occur are generated, thus aiding a designer in their removal. The described formalizations and proofs have been illustrated via the DLX RISC processor.

• Type: Conference
• Year: 1994
• Where: EURODAC
• Authors: Ramayya Kumar, Sofiène Tahar
• Keywords: DLX RISC Processor, EURODAC 1994, Pipeline Conflicts, Risc Cores, VHDL