Title :
Techniques for verifying superscalar microprocessors
Author_Institution :
Cadence Berkeley Lab., USA
Abstract :
J.R. Burch and D.L. Dill (1994) 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
Keywords :
microprocessor chips; DLX architecture; control logic; instruction set architecture; pipelined processor; superscalar microprocessors verification; Automatic control; Automatic logic units; Instruction sets; Laboratories; Logic circuits; Microprocessors; Permission; Polynomials; Process control; Processor scheduling;
Conference_Titel :
Design Automation Conference Proceedings 1996, 33rd
Conference_Location :
Las Vegas, NV
Print_ISBN :
0-7803-3294-6
DOI :
10.1109/DAC.1996.545637
