Abstract
Transformations using retiming and resynthesis operations are the most important and practical (if not the only) techniques used in optimizing synchronous hardware systems. Although these transformations have been studied extensively for over a decade, questions about their optimization capability and verification complexity are not answered fully. Resolving these questions may be crucial in developing more effective synthesis and verification algorithms. This paper settles the above two open problems. The optimization potential is resolved through a constructive algorithm which determines if two given finite state machines (FSMs) are transformable to each other via retiming and resynthesis operations. Verifying the equivalence of two FSMs under such transformations, when the history of iterative transformation is unknown, is proved to be PSPACE-complete and hence just as hard as general equivalence checking, contrary to a common belief. As a result, we advocate a conservative design methodology for the optimization of synchronous hardware systems to ameliorate verifiability. Our analysis reveals some properties about initializing FSMs transformed under retiming and resynthesis. On the positive side, established is a lag-independent bound on the length increase of initialization sequences for FSMs under retiming. It allows a simpler incremental construction of initialization sequences compared to prior approaches. On the negative side, we show that there is no analogous transformation-independent bound when resynthesis and retiming are iterated. Fortunately, an algorithm computing the exact length increase is presented.
This work was supported in part by NSF grant CCR-0312676, the California Micro program, and our industrial sponsors, Fujitsu, Intel, Magma and Synplicity.
Chapter PDF
Similar content being viewed by others
References
De Micheli, G.: Synchronous logic synthesis: algorithms for cycle-time minimization. IEEE Trans. on Computer-Aided Design 10, 63–73 (1991)
El-Maleh, A., Marchok, T.E., Rajski, J., Maly, W.: Behavior and testability preservation under the retiming transformation. IEEE Trans. on Computer-Aided Design 16, 528–543 (1997)
Even, G., Spillinger, I.Y., Stok, L.: Retiming revisited and reversed. IEEE Trans. on Computer-Aided Design 15, 348–357 (1996)
Immerman, N.: Nondeterministic space is closed under complementation. SIAM Journal on Computing 17, 935–938 (1988)
Jones, N.: Space-bounded reducibility among combinatorial problems. Journal of Computer and System Sciences 11, 68–85 (1975)
Kohavi, Z.: Switching and Finite Automata Theory. McGraw-Hill, New York (1978)
Leiserson, C.E., Saxe, J.B.: Optimizing synchronous systems. Journal of VLSI and Computer Systems 1(1), 41–67 (1983) (Spring)
Leiserson, C.E., Saxe, J.B.: Retiming synchronous circuitry. Algorithmica 6, 5–35 (1991)
Malik, S.: Combinational Logic Optimization Techniques in Sequential Logic Synthesis. PhD thesis, University of California, Berkeley (1990)
Malik, S., Sentovich, E.M., Brayton, R.K., Sangiovanni-Vincentelli, A.: Retiming and resynthesis: optimization of sequential networks with combinational techniques. IEEE Trans. Computer-Aided Design 10, 74–84 (1991)
Mneimneh, M.N., Sakallah, K.A., Moondanos, J.: Preserving synchronizing sequences of sequential circuits after retiming. In: Proc. ASP-DAC (January 2004)
Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)
Pixley, C.: A theory and implementation of sequential hardware equivalence. IEEE Trans. Computer-Aided Design 11, 1469–1478 (1992)
Ranjan, R.K.: Design and Implementation Verification of Finite State Systems. Ph.D. thesis, University of California at Berkeley (1997)
Ranjan, R.K., Singhal, V., Somenzi, F., Brayton, R.K.: On the optimization power of retiming and resynthesis transformations. In: Proc. Int’l Conf. on Computer-Aided Design, pp. 402–407 (November 1998)
Savitch, W.: Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences 4, 177–192 (1970)
Singhal, V., Malik, S., Brayton, R.K.: The case for retiming with explicit reset circuitry. In: Proc. Int’l Conf. on Computer-Aided Design, pp. 618–625 (1996)
Singhal, V., Pixley, C., Rudell, R.L., Brayton, R.K.: The validity of retiming sequential circuits. In: Proc. Design Automation Conference, pp. 316–321 (1995)
Touati, H.J., Brayton, R.K.: Computing the initial states of retimed circuits. IEEE Trans. on Computer-Aided Design 12, 157–162 (1993)
Zhou, H., Singhal, V., Aziz, A.: How powerful is retiming? In: Proc. IWLS (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jiang, JH.R. (2005). On Some Transformation Invariants Under Retiming and Resynthesis. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)