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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Verifying a pipelined microprocessor


    Contributors:


    Publication date :

    2000-01-01


    Size :

    722857 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Verifying a Pipelined Microprocessor

    Bickford, M. / IEEE / AIAA | British Library Conference Proceedings | 2000


    Programable Pipelined-Image Processor

    Gennery, D. B. / Wilcox, B. | NTRS | 1986



    Programming a Pipelined Image Processor

    Olson, T. J. / Taylor, J. R. / Lockwood, R. J. | British Library Online Contents | 1996


    IMPROVEMENT OF MICROPROCESSOR COMPLEX SCHEME USING MICROPROCESSOR HARDWARE COMPLEX

    K. I. Yashchuk / S. S. Petrovsky | DOAJ | 2019

    Free access