On Some Transformation Invariants Under Retiming and Resynthesis

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 desi...

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Jie-Hong Roland Jiang
• Keywords: Algorithms, Initialization Sequences, Resynthesis Operations, Synchronous Hardware Systems, TACAS 2005