Verifying a pipelined microprocessor
Mark Bickford · 2002
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.