The practical verification of microprocessor designs

The author describes a research program that is designed to move hardware verification into the mainstream of circuit design. He describes a methodology for microprocessor verification based on a generic interpreter theory. The generic interpreter theory provides a methodological approach to microprocessor specification and verification. He also briefly describes two case studies where the generic interpreter theory was used to specify and verify a microprocessor. These case studies are important because they provide exemplary verifications that engineers can use to guide the use of the generic interpreter theory. The first, AVM-1, is a microprocessor designed and verified as part of a verified chip-set at the University of California, Davis. The second is a reverification of VIPER done as a test of the methodology. Research aimed at integrating verification with VLSI CAD tools is discussed.<>