In this paper we propose a novel refinement-based technique to formally verify data transfer in an asynchronous timing framework. Novel data transfer models are proposed to represent data communication between two locally independent clock domains. As a case study, we apply our technique to verify data transfer in a previously published architecture for globally asynchronous locally synchronous on-chip systems. In this case study, we find several race conditions, hazards, and other dangers that were not mentioned in the original publication, and we find additional delay constraints that avoid some of the detected dangers. © 2001 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Kong, X., Negulescu, R., & Ying, L. W. (2001). Refinement-based formal verification of asynchronous wrappers for independently clocked domains in systems on chip. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2144, 370–385. https://doi.org/10.1007/3-540-44798-9_29
Mendeley helps you to discover research relevant for your work.