Refining abstract equivalence analysis for embedded system design
Harry Hsieh, Felice Balarin · 2002
The synchronous assumption has made it possible to develop efficient procedures for establishing functional equivalence between different implementations in the domains of synchronous circuits and synchronous reactive systems. This notion is extended to embedded systems that do not satisfy the synchronous assumption inside their boundaries but only at the interface with the environment. Efficient, but conservative, synchronous equivalence analysis algorithms have been developed. In this work, we propose extensions to these algorithms that allow trading off the complexity with the conservativeness of the results.