A Hierarchical Methodology for Verifying Microprogrammed Microprocessors

To date, several microprocessors have been verified using formal methods. The only successfulverification efforts, however, have been on relatively simple microprocessor architectures (fewer than32 words ofmicro instruction store, small instruction set, lhnitedfeaturesf orsupportingo peratings ystems,etc.). Thegoal of the research reported here is to develop methodologies for verifying much larger architectures and demonstrate their applicabilityby verifying such a microprocessor. This paper presentsa hieratical methodology for decomposing microprocessor verifications which reduces thenecessary effort bymorethanrm order of magnitude. A secondary result of the research is a veritied microengine that can be used to quickly implement verified microprocessorswith varied architectures.