Title :
Correct-by-construction asynchronous implementation of modular synchronous specifications
Author :
Potop-Butucaru, Dumitru ; Caillaud, Benoît
Author_Institution :
IRISA, Campus Univ. de Beaulieu, Rennes, France
Abstract :
We introduce a model for the representation of asynchronous implementations of synchronous specifications. The model covers classical implementations, where a notion of global synchronization is preserved by means of signaling, and globally asynchronous, locally synchronous (GALS) implementations where the global clock is removed. Our model offers a unified framework for reasoning about two essential correctness properties of an implementation: the preservation of semantics and the absence of deadlocks.
Keywords :
asynchronous circuits; formal specification; synchronisation; asynchronous implementation; global clock; global synchronization; modular synchronous specification; Asynchronous communication; Circuit testing; Clocks; Computer architecture; Concurrent computing; Design methodology; Functional programming; Power system modeling; Synchronization; System recovery;
Conference_Titel :
Application of Concurrency to System Design, 2005. ACSD 2005. Fifth International Conference on
Print_ISBN :
0-7695-2363-3
DOI :
10.1109/ACSD.2005.10
