• DocumentCode
    1747862
  • Title

    Scalable hybrid verification of complex microprocessors

  • Author

    Mneimneh, Maher ; Aloul, Fadi ; Weaver, Chris ; Chatterjee, Saugata ; Sakallah, Karem ; Austin, Todd

  • Author_Institution
    Michigan Univ., Ann Arbor, MI, USA
  • fYear
    2001
  • fDate
    2001
  • Firstpage
    41
  • Lastpage
    46
  • Abstract
    We introduce a new verification methodology for modern microprocessors that uses a simple checker processor to validate the execution of a companion high-performance processor. The checker can be viewed as an at-speed emulator that is formally verified to be compliant to an ISA specification. This verification approach enables the practical deployment of formal methods without impacting overall performance.
  • Keywords
    Boolean functions; development systems; formal verification; logic CAD; microprocessor chips; ISA specification; at-speed emulator; checker processor; complex microprocessors; formal methods; scalable hybrid verification; Batteries; Computer bugs; Degradation; Instruction sets; Microprocessors; Modems; Out of order; Permission; Testing; Virtual manufacturing;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Design Automation Conference, 2001. Proceedings
  • ISSN
    0738-100X
  • Print_ISBN
    1-58113-297-2
  • Type

    conf

  • DOI
    10.1109/DAC.2001.156105
  • Filename
    935474