Title :
Processor validation: a top-down approach
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;
Journal_Title :
Potentials, IEEE
DOI :
10.1109/MP.2005.1405799