Techniques for Verifying Superscalar Microprocessors

Burch and Dill [3] described an automatic method for verifying a pipelined processor against its instruction setarchitecture(ISA). We describethree techniquesfor 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.

• Type: Conference
• Year: 1996
• Where: DAC
• Authors: Jerry R. Burch
• Keywords: Automatic Method, Automatic Verification, Computer Architecture, DAC 1996, Superscalar Implementation