Transformation-Based Verification Using Generalized Retiming

Andreas Kuehlmann Jason Baumgartner

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

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.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems