Title :
Verification of a Data Synchronization Circuit For All Time
Author :
Brown, Geoffrey M.
Author_Institution :
Indiana Univ., IN
Abstract :
This paper presents a model and automated proof for a synchronizer circuit that is commonly used to reliably transfer data across clock domains. In contrast with previous work, this paper describes a proof that is valid for all clock rates and phases meeting modest constraints. Furthermore, the proof was realized with an existing model checker - SAL
Keywords :
clocks; formal verification; logic circuits; logic design; synchronisation; SAL model checker; clock domain; data synchronization circuit verification; synchronizer circuit automated proof; Analytical models; Bridge circuits; Circuit analysis; Clocks; Flip-flops; Metastasis; Protocols; Synchronization; Timing; Transmitters;
Conference_Titel :
Application of Concurrency to System Design, 2006. ACSD 2006. Sixth International Conference on
Conference_Location :
Turku
Print_ISBN :
0-7695-2556-3
DOI :
10.1109/ACSD.2006.35
