Verification and re-design of communication interfaces with heterogeneous timing
Weidong Larry Ying · eScholarship@McGill (McGill) · 2001
In this thesis we use a novel refinement-based technique to formally verify data transfer in an asynchronous timing framework. Novel data transfer models are proposed to represent the implicit relationship between clock and data validity events. We construct comprehensive implementation models for a previously published GALS architecture for on-chip systems [MVK+99]. Applying our techniques on this claimed to be hazard-free architecture, we find several hazards, and other dangers, together with additional delay constraints to avoid some of the detected dangers. We further exam re-design issues of an existing GALS system as compact design, internal structure optimization and reduced power consumption. Exhaustive verifications are applied to re-designed asynchronous wrapper circuits using our proposed refinement-based technique to ensure hazard-free operation. We explore a strategy to resolve relative timing conflicts by implementing detected chain constraints as new circuit components to be integrated with the original design. This method is applied on two design cases to demonstrate its benefits and tradeoffs.