Applications of hierarchical verification in model checking

Abstract

The LTL model checker that we use provides sound decomposition mechanisms within a purely model checking environment.We have exploited these mechanisms to successfully verify a wide spectrum of large and complex circuits. This paper describes a variety of the decomposition techniques that we have used as part of a large industrial formal verification effort on the Intel Pentium®4 (Willamette) processor.