Strong Retiming Equivalence of Synchronous Schemes

摘要

Strong retiming equivalence is the join of two basic equivalence relations of synchronous schemes: strong equivalence and retiming equivalence, which play an important role in the optimization of synchronous systems. Each of these equivalences is characterized separately in an algebraic/category theoretic framework, and the characterization is carried over to the join of them. Tree-reducible schemes are introduced to facilitate the proof that strong retiming equivalence is decidable.