On Some Transformation Invariants Under Retiming and Resynthesis

  • Jie-Hong R. Jiang
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


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.


  1. 1.
    De Micheli, G.: Synchronous logic synthesis: algorithms for cycle-time minimization. IEEE Trans. on Computer-Aided Design 10, 63–73 (1991)CrossRefGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Even, G., Spillinger, I.Y., Stok, L.: Retiming revisited and reversed. IEEE Trans. on Computer-Aided Design 15, 348–357 (1996)CrossRefGoogle Scholar
  4. 4.
    Immerman, N.: Nondeterministic space is closed under complementation. SIAM Journal on Computing 17, 935–938 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Jones, N.: Space-bounded reducibility among combinatorial problems. Journal of Computer and System Sciences 11, 68–85 (1975)zbMATHMathSciNetCrossRefGoogle Scholar
  6. 6.
    Kohavi, Z.: Switching and Finite Automata Theory. McGraw-Hill, New York (1978)zbMATHGoogle Scholar
  7. 7.
    Leiserson, C.E., Saxe, J.B.: Optimizing synchronous systems. Journal of VLSI and Computer Systems 1(1), 41–67 (1983) (Spring)zbMATHGoogle Scholar
  8. 8.
    Leiserson, C.E., Saxe, J.B.: Retiming synchronous circuitry. Algorithmica 6, 5–35 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Malik, S.: Combinational Logic Optimization Techniques in Sequential Logic Synthesis. PhD thesis, University of California, Berkeley (1990)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    Mneimneh, M.N., Sakallah, K.A., Moondanos, J.: Preserving synchronizing sequences of sequential circuits after retiming. In: Proc. ASP-DAC (January 2004)Google Scholar
  12. 12.
    Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)zbMATHGoogle Scholar
  13. 13.
    Pixley, C.: A theory and implementation of sequential hardware equivalence. IEEE Trans. Computer-Aided Design 11, 1469–1478 (1992)CrossRefGoogle Scholar
  14. 14.
    Ranjan, R.K.: Design and Implementation Verification of Finite State Systems. Ph.D. thesis, University of California at Berkeley (1997)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Savitch, W.: Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences 4, 177–192 (1970)zbMATHMathSciNetCrossRefGoogle Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    Touati, H.J., Brayton, R.K.: Computing the initial states of retimed circuits. IEEE Trans. on Computer-Aided Design 12, 157–162 (1993)CrossRefGoogle Scholar
  20. 20.
    Zhou, H., Singhal, V., Aziz, A.: How powerful is retiming? In: Proc. IWLS (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Jie-Hong R. Jiang
    • 1
  1. 1.Department of Electrical Engineering and Computer SciencesUniversity of CaliforniaBerkeley

Personalised recommendations