The linear temporal 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 circuits. This paper describes a variety of the
decomposition strategies that we have used as part of a multi-year
industrial formal verification effort. The strategies generally use
structural decomposition and cone-of-influence reductions to
transform the verification of a single, large property into the
verification of a number of smaller properties. We have also
exploited symmetry to write parameterized properties that we verify
over regular structures such as arrays.
