面向SoC系统芯片中跨时钟域设计的模型检验方法

• 作者: 佟冬 冯毅 刘丹 易江芳 程旭
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 形式化验证 模型检验 跨时钟域设计 线性时序逻辑
• 年，卷（期）: 2008,（5）
• 所属期刊栏目: 学术论文
• 页码范围: 886-892
• 页数: 7页
• 分类号: TP302
• 字数: 7198字
• 语种: 中文
• DOI: 10.3321/j.issn:0372-2112.2008.05.010

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘丹	北京大学微处理器研究与开发中心	93	447	11.0	16.0
2	程旭	北京大学微处理器研究与开发中心	85	436	11.0	16.0
3	佟冬	北京大学微处理器研究与开发中心	51	284	8.0	14.0
4	易江芳	北京大学微处理器研究与开发中心	10	88	5.0	9.0
5	冯毅	北京大学微处理器研究与开发中心	5	25	3.0	5.0