A hierarchical methodology for verifying microprogrammed microprocessors
- 1 January 1990
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 345-357
- https://doi.org/10.1109/risp.1990.63863
Abstract
To date, several microprocessors have been verified using formal methods. The only successful verification efforts, however, have been on relatively simple microprocessor architectures (fewer than 32 words of micro instruction store, small instruction set, limited features for supporting operating systems, etc.). The goal of the research reported is to develop methodologies for verifying much larger architectures and demonstrate their applicability verifying such a microprocessor. A hierarchical methodology is presented for decomposing microprocessor verifications which reduces the necessary effort by more than an order of magnitude. A secondary result of the research is a verified microengine that can be used to quickly implement verified microprocessors with varied architectures.Keywords
This publication has 4 references indexed in Scilit:
- Reverification of a microprocessorPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A Proof of Correctness of the Viper Microprocessor: The First LevelPublished by Springer Nature ,1988
- Implementing Safety-Critical Systems: The VIPER MicroprocessorPublished by Springer Nature ,1988
- Logic programming and digital circuit analysisThe Journal of Logic Programming, 1987