Synchronous equivalence for embedded systems: a tool for design exploration
Harry Hsieh, Alberto Luigi Sangiovanni-Vincentelli, Felice Balarin, Luciano Lavagno · 1999
Design exploration consists of analyzing several alternative implementations of the "same" function to determine the most desirable one. A fundamental question is whether an "implementation " is consistent with the high-level specification or whether two implementations are "equivalent". In this paper, we define synchronous equivalence for embedded systems that strongly resembles the concept of functional equivalence for sequential circuits. We then present equivalence analysis algorithms that are of low polynomial complexity. We show an example of application of the algorithms to a real-life design (a shock absorber controller) and demonstrate that synchronous equivalence opens design exploration avenue s uncharted before.