In this paper we present the application of generalized retiming for
temporal property checking. Retiming is a structural transformation
that relocates the state holding elements, i.e., registers, in a
circuit-based design representation without changing its actual
input-output behavior. We discuss the application of retiming to
minimize the number of registers with the goal of increasing the
capacity of symbolic state traversal. In particular, we demonstrate
that in verification the classical definition of retiming can be
generalized by relaxing the notion of design equivalence and
implementability. This includes (1) omitting the need for equivalent
reset states by using an initialization stump, (2) supporting negative
registers, handled as general functional relations to future time
frames, and (3) eliminating peripheral registers by converting them
into simple temporal offsets. The presented results using standard
benchmark circuits and industrial designs demonstrate that the
application of retiming in verification can significantly increase the
capacity of symbolic state space traversal. Our experiments also
demonstrate that the repeated use of retiming interleaved with other
structural simplifications can yield reductions beyond those possible
with single applications of the individual approaches. This result
suggests that a tool architecture based on re-entrant transformation
engines can potentially decompose and solve verification problems that
otherwise are infeasible.
