SoC系统芯片跨时钟域设计的RTL模型验证策略

本文主要探讨了在面向SoC系统芯片的设计中，特别是在处理跨时钟域(Clock Domain Crossing, CDC)问题时的模型验证方法。SoC系统集成度高，涉及多个时钟域间的通信，这对设计者提出了挑战，因为传统的方法在RTL (Register Transfer Level) 阶段往往无法全面验证这些复杂的时序交互。 首先，作者提出了一种新的方法，即通过构建等效电路来描述亚稳态现象。亚稳态是由于跨时钟域信号延迟引起的，它在实际设计中可能导致潜在的逻辑错误。这个电路模型使得在RTL验证阶段能够准确模拟亚稳态的影响，从而提高验证的准确性。 接着，文章引入了线性时序逻辑，这是一种有效的工具，用于规范跨时钟域设计的行为。通过线性化时序逻辑，设计者可以更清晰地定义信号在不同时钟周期之间的转换规则，使得模型检查更为直观和高效。 为了缓解模型检验过程中因寄存器数量增加导致的空间爆炸问题，本文提出了一种创新策略。一是基于输入信号的迁移关系分组策略，通过合理组织和归类输入信号，减少了模型复杂度，减轻了空间需求。二是基于数学归纳的优化策略，通过递归分析和归纳法，逐步缩小搜索空间，降低了验证的时间复杂度。 实验结果表明，本文的方法在RTL验证阶段显著提高了对跨时钟域设计功能错误的检测能力。相比于传统的指数级增长，验证时间随着寄存器数量的增加呈现出近似多项式级的增长，这意味着验证效率得到了显著提升，这对于大型SoC系统的设计验证具有重要的实践意义。 这篇论文为SoC系统芯片中跨时钟域设计的模型验证提供了一种有效且高效的解决方案，对于保证系统的正确性和设计效率具有重要的推动作用。关键词包括形式化验证、模型检验、跨时钟域设计以及线性时序逻辑，这表明了作者的研究集中在高级设计方法和验证技术上。