Synchronous approach to the functional equivalence of embedded system implementations

Design space exploration is the process of analyzing several functionally e quivalent alternatives to determine the most suitable one, A fundamental qu estion is whether an implementation is consistent with the high-level speci fication or whether two implementations are "equivalent." The synchronous a ssumption has made it possible to develop efficient procedures for establis hing functional equivalence between different implementations in the domain s of synchronous circuits and synchronous reactive systems. We extend this notion to embedded systems that do not satisfy the synchronous assumption i nside their boundaries but only at the interface with the environment. Leve raging this property, we define synchronous equivalence for embedded system s that strongly resembles the concept of functional equivalence for sequent ial circuits. We develop efficient synchronous equivalence analysis algorit hms for embedded system designs. The efficiency comes from analyzing the be havior statically on abstract representations, at a cost that some of the n egative results may be false. i.e. the analysis is conservative. We develop primitives for making the representation more/less abstract, trading off c omplexity of the algorithms with the conservativeness of the results. We ap ply our analysis algorithms to an ATM switch and demonstrate that synchrono us equivalence opens design exploration avenues uncharted before.