Verifying a pipelined microprocessor

Author

Bickford, Mark

Author_Institution

Odyssey Res. Associates Inc., Ithaca, NY, USA

Volume

1

fYear

2000

fDate

2000

Abstract

Demonstrates the effectiveness of the Larch/VHDL verification system by verifying a commercial microprocessor design. The National Security Agency (NSA) gave us the opportunity to verify a design of over 10,000 lines of VHDL source code, written by Motorola engineers, called the LRP15O. This design was an implementation of a microprocessor instruction set and specification called ARM7 from Advanced RISC Machines. It was an ideal challenge. No microprocessor design of this scale had been formally verified, and certainly no design of this size had been verified directly from VHDL or any other standardized hardware description language

Keywords

formal verification; hardware description languages; instruction sets; integrated circuit design; microprocessor chips; pipeline processing; reduced instruction set computing; ARM7; Advanced RISC Machines; LRP15O; Larch/VHDL verification system; Motorola; microprocessor design; microprocessor instruction set; pipelined microprocessor; Clocks; Design engineering; Error correction; Formal specifications; Hardware design languages; Mathematical model; Microprocessors; National security; Reduced instruction set computing; Very high speed integrated circuits;

fLanguage

English

Publisher

ieee

Conference_Titel

Digital Avionics Systems Conference, 2000. Proceedings. DASC. The 19th

Conference_Location

Philadelphia, PA

Print_ISBN

0-7803-6395-7

Type

conf

DOI

10.1109/DASC.2000.886876

Filename

886876