摘要：传统方法无法在RTL验证阶段全面验证SoC系统芯片中的跨时钟域设计．为解决此问题，本文首先提出描述亚稳态现象的等价电路实现，用以在RTL验证中准确体现亚稳态现象的实际影响；然后使用线性时序逻辑对跨时钟域设计进行设计规范的描述；为缓解模型检验的空间爆炸问题，进一步针对跨时钟域设计的特点提出基于输入信号的迁移关系分组策略和基于数学归纳的优化策略．实验结果表明本文提出的方法不仅可以在RTL验证阶段有效地发现跨时钟域设计的功能错误，而且可以使验证时间随实验用例中寄存器数量的递增趋势从近似指数级增长减小到近似多项式级增长．

关键词：形式化验证 模型检验 跨时钟域设计 线性时序逻辑 

单位：北京大学微处理器研究与开发中心; 北京100871