电子学报 ›› 2009, Vol. 37 ›› Issue (2): 258-265.

• 论文 • 上一篇    下一篇

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

冯 毅, 许经纬, 易江芳, 佟 冬, 程 旭   

  1. 北京大学微处理器研究与开发中心,北京 100871
  • 收稿日期:2008-01-03 修回日期:2008-06-25 出版日期:2009-02-25 发布日期:2009-02-25

Property Generation Method for Model Checking on Clock Domain Crossing Design

FENG Yi, XU Jing-wei, YI Jiang-fang, TONG Dong, CHENG Xu   

  1. Micro-Processor Research and Development Center,Peking University,Beijing 100871,China
  • Received:2008-01-03 Revised:2008-06-25 Online:2009-02-25 Published:2009-02-25

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

关键词: 形式化验证, 模型检验, 跨时钟域设计, 电路特性生成

Abstract: Verification on Clock Domain Crossing(CDC)design is crucial to the SoC functional verification.Traditional model checking methods on CDC design do not consider the completeness of properties.However,generating complete design properties is the basis for model checking,and incomplete properties would lead to bug escape.To generate complete properties for CDC design,we first propose a finite state automaton based property generation method.Then,to solve the exponential explosive problem,we propose a metastability based data type reduction strategy.Experiment results on two typical CDC designs show that,our approach not only achieves 100% property coverage,but also discovers a bug that escaped by traditional methods.Meanwhile,the verification time for model checking is greatly reduced.

Key words: formal verification, model checking, clock domain crossing design, property generation

中图分类号: