Title :
Formal verification for microprocessors with extendable instruction set
Author :
Sawitzki, S. ; Spallek, R.G. ; Schönherr, J. ; Straube, B.
Author_Institution :
Inst. of Comput. Eng., Tech. Univ. Dresden, Germany
Abstract :
The correctness of processors is a key for their application. Although some verification methods were developed and successfully applied to conventional microprocessors, only a few of them were used in the context of application specific devices. This work introduces a formal verification approach for a reconfigurable microprocessor with extendable instruction set. The application of this approach is demonstrated using register transfer description of the CoMPARE processor and the Stanford Validity Checker as prover. Some undesired side effects of different instructions that were not discovered during the simulation were found by the verification process. In addition some deficiencies of the hardware description notation as specification formalism were shown
Keywords :
formal verification; hardware description languages; instruction sets; microprocessor chips; reconfigurable architectures; CoMPARE processor; Stanford Validity Checker; extendable instruction set; formal verification; hardware description notation; reconfigurable microprocessor; register transfer description; Application software; Arithmetic; Binary decision diagrams; Communication system control; Field programmable gate arrays; Formal verification; Microprocessors; Prototypes; Reconfigurable logic; Registers;
Conference_Titel :
Application-Specific Systems, Architectures, and Processors, 2000. Proceedings. IEEE International Conference on
Conference_Location :
Boston, MA
Print_ISBN :
0-7695-0716-6
DOI :
10.1109/ASAP.2000.862377
