A top-down methodology for microprocessor validation

Equivalence checking is a formal technique that is popular in industry today. Typically, this technique involves comparing the implementation to a set of Boolean equations or comparing an optimized circuit to the original circuit. Symbolic simulation is an efficient technique that bridges the gap between traditional simulation and full-fledged formal verification. This paper presents a top-down methodology for validation of microprocessors using a combination of symbolic simulation and equivalence checking.