Sciweavers

CAV
2001
Springer

Transformation-Based Verification Using Generalized Retiming

14 years 1 months ago
Transformation-Based Verification Using Generalized Retiming
In this paper we present the application of generalized retiming for temporal property checking. Retiming is a structural transformation that relocates 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 the classical definition of retiming can be generalized for verification by relaxing the notion of design equivalence and physical implementability. This includes (1) omitting the need for equivalent reset states by using an initialization stump, (2) supporting negative registers, handled by a general functional relation to future time frames, and (3) eliminating peripheral registers by converting them into simple temporal offsets. The presented results demonstrate that the application of retiming in verification can significantly increase the capacity of symb...
Andreas Kuehlmann, Jason Baumgartner
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2001
Where CAV
Authors Andreas Kuehlmann, Jason Baumgartner
Comments (0)