Synchronous equivalence for embedded systems: a tool for design exploration

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". 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 up design exploration avenues uncharted before.