• DocumentCode
    1513465
  • Title

    Practical formal verification in microprocessor design

  • Author

    Jones, Robert B. ; O´leary, John W. ; Seger, Carl-Johan H. ; Aagaard, Mark D. ; Melham, Thomas F.

  • Author_Institution
    Intel Corp., Hillsboro, OR, USA
  • Volume
    18
  • Issue
    4
  • fYear
    2001
  • Firstpage
    16
  • Lastpage
    25
  • Abstract
    Practical application of formal methods requires more than advanced technology and tools; it requires an appropriate methodology. A verification methodology for data-path-dominated hardware combines model checking and theorem proving in a customizable framework. This methodology has been effective in large-scale industrial trials, including verification of an IEEE-compliant floating-point adder
  • Keywords
    formal verification; logic design; microprocessor chips; theorem proving; IEEE-compliant floating-point adder; customizable framework; data-path-dominated hardware; formal methods; formal verification; large-scale industrial trials; microprocessor design; model checking; theorem proving; verification methodology; Acoustical engineering; Adders; Circuit simulation; Circuit testing; Debugging; Design engineering; Documentation; Formal verification; Large-scale systems; Microprocessors;
  • fLanguage
    English
  • Journal_Title
    Design & Test of Computers, IEEE
  • Publisher
    ieee
  • ISSN
    0740-7475
  • Type

    jour

  • DOI
    10.1109/54.936245
  • Filename
    936245
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1513465