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.