A hierarchical methodology for verifying microprogrammed microprocessors

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