面向模型检验的跨时钟域设计电路特性生成方法

• 作者: 佟冬 冯毅 易江芳 程旭 许经纬
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 形式化验证 模型检验 跨时钟域设计 电路特性生成
• 年，卷（期）: 2009,（2）
• 所属期刊栏目: 学术论文
• 页码范围: 258-265
• 页数: 8页
• 分类号: TP302
• 字数: 6656字
• 语种: 中文
• DOI: 10.3321/j.issn:0372-2112.2009.02.004

摘要

对跨时钟域设计进行功能验证是SoC验证中的难点问题.传统的面向跨时钟域设计的模型检验方法并没有充分考虑电路特性描述的完整性问题,然而制订完整的电路特性是模型检验有效性的基础,不全面的电路特性描述将可能隐藏设计错误.为生成完整的描述跨时钟域设计的电路特性,本文首先提出基于有限状态自动机的电路特性生成方法;然后为缓解状态空间爆炸问题,提出基于亚稳态的数值化简策略.通过对两个典型的跨时钟域设计进行实验的结果表明,采用本文方法不仅能够达到100%的电路特性覆盖率,而且可以发现被传统方法隐藏的功能错误.同时模型检验的时间代价也能够得到大幅度降低.

作者信息

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