关键词: 跨时钟域设计，基于断言的验证，PSI_属性说明语言，符号模型检查，LTL线性时序逻辑

Abstract: With the increasing number of clock domains and CDC signals in today's high-performance,low-power SOC,the design and verification of CDC problem become more and more important. Traditional verification methods can notfind a comprehensive cross-clock domain design of functional errors in the RTL stage. In this paper, we dicussed 5 types of CDC synchronizer circuit templates of our chip, and proposed hiberarchy verification method: structural analysis, assertion-based verification, and formal verification. Taped sample chip tests show all CDC designs work right, and demonstrate that design and verification method arc effective and complete.

Key words: Clock domain crossing design,Asscrtion-based verification,PSI_(Property Specification Language)，Symbolie model checking,LTL logic