Methodology and Experience of Simulation-Based Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications

Abstract — In this paper we describe a methodology and ex-perience of simulation-based verification of microprocessor units based on cycle-accurate contract specifications. Such specifica-tions describe behavior of a unit in the form of preconditions and postconditions of microoperations. We have successfully applied the methodology to several units of the industrial microprocessor. The experience shows that cycle-accurate contract specifications are very suitable for simulation-based verification, since, first, they represent functional requirements on a unit in compre-hensible declarative form, and second, they make it possible to automatically construct test oracles which verify unit correctness. I