Experience with term level modeling and verification of the M*CORE TM microprocessor core

The paper describes the use of term-level modeling and verification of an industrial microprocessor, M*CORE^TM which is a limited dual-issue, super-scalar processor with instruction prefetching mechanism, deep pipeline, multicycle functional units, speculation and interlocks. Term-level modeling uses terms, uninterpreted functions and predicates to abstract the data path complexity of the microprocessor. The verification of the control path is carried out almost mechanically with the aid of CMU-EVC, an extremely efficient decision procedure based on the Logic of Positive Equality with Uninterpreted Functions (PEUF). The verification effort resulted in detection of a couple of non-trivial bugs in the microarchitecture in design exploration phase of the design. The paper demonstrates the effectiveness of CMU-EVC for automated verification of real-life microprocessor designs and also points out some of the challenges and the future work that need to be addressed in term-level modeling and verification of microprocessors using CMU-EVC