Title :
A methodology for validation of microprocessors using equivalence checking
Author :
Mishra, Prabhat ; Dutt, Nikil
Author_Institution :
Archit. & Compilers for Embedded Syst. Lab., California Univ., Irvine, CA, USA
Abstract :
As embedded systems continue to face increasingly higher performance requirements, deeply pipelined processor architectures are being employed to meet desired system performance. Validation of such processor architectures is one of the most complex and expensive tasks in the current systems-on-chip design process. A significant bottleneck in the validation of such systems is the lack of a golden reference model. We present an architecture description language (ADL) driven methodology for generating golden reference model. We use EXPRESSION ADL to capture the structure and behavior of the processor. The synthesizable register transfer language (RTL) description of the architecture is generated from the ADL specification. The generated RTL description is used as a golden reference model for verifying the correctness of the implementation using equivalence checking. We applied our methodology on a RISC DLX architecture to demonstrate the usefulness of our approach.
Keywords :
embedded systems; formal verification; microcomputers; pipeline processing; programming languages; reduced instruction set computing; system-on-chip; EXPRESSION ADL; RISC DLX architecture; RTL; architecture description language; embedded system; equivalence checking; golden reference model; microprocessors validation; pipelined processor; register transfer language; systems-on-chip design; Application software; Architecture description languages; Computer architecture; Embedded system; Feedback; Hardware design languages; Microprocessors; Process design; Reduced instruction set computing; Space exploration;
Conference_Titel :
Microprocessor Test and Verification: Common Challenges and Solutions, 2003. Proceedings. 4th International Workshop on
Print_ISBN :
0-7695-2045-6
DOI :
10.1109/MTV.2003.1250267