Towards a methodology for the formal hierarchical verification of RISC processors
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
A general methodology, based on a hierarchical model of interpreters, is presented for formally verifying RISC cores. The abstraction levels used by a designer in the implementation of RISC cores, namely the instruction set level, the pipeline stage level, the phase level and the hardware implementation, are mirrored by this hierarchical model. The use of this model allows us to successively prove the correctness between two neighboring levels of abstractions, so that the verification process is simplified. The parallelism in the execution of the instructions, resulting from the pipelined architecture of RISCs is handled by splitting the proof into simplified steps. The first step shows that, under certain assumptions, no conflicts can occur between simultaneously executed instructions, and the second step shows that each instruction is implemented correctly by the sequential execution of its pipeline steps Author(s) Tahar, S. Inst. of Comput. Design & Fault Tolerance, Karlsruhe Univ., Germany Kumar, R.Keywords
This publication has 4 references indexed in Scilit:
- Headroom and legroom in the 80960 architecturePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Structuring and automating hardware proofs in a higher-order theorem-proving environmentFormal Methods in System Design, 1993
- A Formalization of a Hierarchical Model for RISC ProcessorsPublished by Springer Nature ,1993
- Specification and verification of digital systems using higher-order predicate logicIEE Proceedings E Computers and Digital Techniques, 1986