Preserving synchronizing sequences of sequential circuits after retiming

ABSTRACT

We propose a novel approach to preserve the synchronizing sequences of a circuit after retiming. The significance of this problem stems from the necessity of maintaining correct initialization of circuits after retiming optimizations. It has been previously shown that forward retiming moves across fanout stems can destroy a synchronizing sequence. We build on this observation and introduce the notion of "invalid states" that might arise due to forward moves. We show that the set of synchronizing sequences of a given circuit can be preserved by modifying transitions from those invalid states. We present an algorithm that implicitly computes the set of invalid states. Then, we describe a post-retiming synthesis step that incrementally resynthesizes some next-state functions to alter the behavior of invalid states to ensure correct post-retiming initialization. We report promising experimental results on the ISCAS 89 benchmarks and on a set of retimed circuits from an Intel Pentium-III class microprocessor.

REFERENCES

• 1: Stephen Brookes, Using fixed-point semantics to prove retiming lemmas, Formal Methods in System Design, v.2 n.1, p.73-91, Feb. 1993 [doi>10.1007/BF01383944]
• 2: Olivier Coudert, and Jean Christophe Madre, "Symbolic Computation of the Valid States of a Sequential Machine: Algorithms and Discussion," in Proceedings of the International Workshop on Formal Methods in VLSI Design, January 1991.
• 3: A. El-Maleh, T. Marchok, J. Rajski, and W. Maly, "Behavior and Testability Preservation Under the Retiming Transformation," in IEEE Transactions on Computer-Aided Design, vol. 16, pp. 528--543, May 1997.
• 4: Guy Even, The retiming lemma: a simple proof and applications, Integration, the VLSI Journal, v.20 n.2, p.123-137, March 1996 [doi>10.1016/0167-9260(95)00021-6]
• 5: C. E. Leiserson and J. B. Saxe, "Retiming Synchronous Circuitry," Algorithmica, vol. 6, pp. 5--35, 1991.
• 6: M. Mneimneh and K. Sakallah, "REVERSE: Efficient Sequential Verification for Retiming," International Workshop on Logic Synthesis, 2003.
• 7: E. Sentovich, K. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. Stephen, R. Brayton, and A. Sangiovanni-Vincentelli, "SIS: A System for Sequential Circuit Synthesis." University of California, Berkeley, Tech. Report, May 1994.
• 8: Vigyan Singhal , Carl Pixley , Richard L. Rudell , Robert K. Brayton, The validity of retiming sequential circuits, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.316-321, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217548]
• 9: F. Somenzi, "CUDD: CU Decision Diagram Package Release 2.3.1," Technical Report, University of Colorado at Boulder, 2001.