• DocumentCode
    1246992
  • Title

    Processor validation: a top-down approach

  • Author

    Mishra, Prabhat

  • Volume
    24
  • Issue
    1
  • fYear
    2005
  • Firstpage
    29
  • Lastpage
    33
  • Abstract
    This work presents the design validation techniques for microprocessors. The verification effectiveness validates the design implementation using a combination of simulation techniques and formal methods. This article presents a top-down validation methodology that complements existing bottom-up verification techniques. The validation team applies model checking to a high-level description of the design abstracted from the RTL implementation. Formal verification uses a formal language to describe the system. The specification for the formal verification comes from the architecture description; the implementation can come from either the architecture specification or the abstracted design. A top-down methodology for validating microprocessors using a combination of symbolic simulation and equivalence checking is presented. Specification-driven hardware generation and validation of design implementation using equivalence checking has one limitation: the structure of the generated hardware reference model is similar to that of implementation.
  • Keywords
    formal specification; formal verification; microprocessor chips; reverse engineering; symbol manipulation; time to market; RTL implementation; design abstraction; design validation technique; equivalence checking; formal language; formal method; high-level description; microprocessor top-down validation methodology; processor formal verification; processor model checking; specification-driven hardware generation reference model; symbolic simulation; Algorithm design and analysis; Automata; Circuit simulation; Computer architecture; Explosions; Feedback; Formal verification; Microprocessors; Performance analysis; State-space methods;
  • fLanguage
    English
  • Journal_Title
    Potentials, IEEE
  • Publisher
    ieee
  • ISSN
    0278-6648
  • Type

    jour

  • DOI
    10.1109/MP.2005.1405799
  • Filename
    1405799