Abstract
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 symbolic state 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 would be infeasible.
Chapter PDF
Similar content being viewed by others
References
O. Coudert, C. Berthet, and J. C. Madre, “Verification of synchronous sequential machines based on symbolic execution,” in International Workshop on Automatic Verification Methods for Finite State Systems, Springer-Verlag, June 1989.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic model checking: 1020 states and beyond,” in IEEE Symposium on Logic in Computer Science, pp. 428–439, IEEE, June 1990.
T. Niermann and J. H. Patel, “HITEC: A test generation package for sequential circuits,” in The European Conference on Design Automation, pp. 214–218, IEEE, February 1991.
C. Leiserson and J. Saxe, “Retiming synchronous circuitry,” Algorithmica, vol. 6, pp. 5–35, 1991.
J. A. Darringer, D. Brand, J. V. Gerbi, W. H. Joyner, and L. H. Trevillyan, “Logic synthesis through local transformations,” IBM Journal on Research and Development, vol. 25, pp. 272–280, July 1981.
A. Gupta, P. Ashar, and S. Malik, “Exploiting retiming in a guided simulation based validation methodology,” in Correct Hardware Design and Verification Methods (CHARME’99), pp. 350–353, September 1999.
S. Malik, E. M. Sentovich, R. K. Brayton, and A. Sangiovanni-Vincentelli, “Retiming and resynthesis: Optimizing sequential networks with combinational techniques,” IEEE Transactions on Computer-Aided Design, vol. 10, pp. 74–84, January 1991.
G. Hasteer, A. Mathur, and P. Banerjee, “Efficient equivalance checking of multi-phase designs using retiming,” in IEEE International Conference on Computer-Aided Design, pp. 557–561, November 1998.
J. Baumgartner, A. Tripp, A. Aziz, V. Singhal, and F. Andersen, “An abtraction algorithm for the verification of generalized C-slow designs,” in Conference on Computer Aided Verification (CAV’00), pp. 5–19, July 2000.
C. Leiserson and J. Saxe, “Optimizing synchronous systems,” Journal of VLSI and Computer Systems, vol. 1, pp. 41–67, January 1983.
H. J. Touati and R. K. Brayton, “Computing the initial states of retimed circuits,” IEEE Transactions on Computer-Aided Design, vol. 12, pp. 157–162, January 1993.
G. Even, I. Y. Spillinger, and L. Stok, “Retiming revisited and reversed,” IEEE Transactions on Computer-Aided Design, vol. 15, pp. 348–357, March 1996.
G. Cabodi, S. Quer, and F. Somenzi, “Optimizing sequential verification by retiming transformations,” in 37th ACM/IEEE Design Automation Conference, pp. 601–606, June 2000.
A. Kuehlmann, M. K. Ganai, and V. Paruthi, “Circuit-based Boolean reasoning,” in Proceedings of the 38th ACM/IEEE Design Automation Conference, ACM/IEEE, June 2001.
M. S. Hung, W. O. Rom, and A. Waren, Optimization with IBM OSL. Scientific Press, 1993.
The VIS Group, “VIS: A system for verification and synthesis,” in Conference on Computer Aided Verification (CAV’96), pp. 428–432, Springer-Verlag, July 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kuehlmann, A., Baumgartner, J. (2001). Transformation-Based Verification Using Generalized Retiming. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_10
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive