Techniques for verifying superscalar microprocessors

Abstract

Burch and Dill [3] described an automatic method for verifying a pipelined processor against its instruction set architecture (ISA). We describe three techniques for improving this method. We show how the combination of these techniques allows for the automatic verification of the control logic of a pipelined, superscalar implementation of a subset of the DLX architecture.