摘要
对跨时钟域设计进行功能验证是SoC验证中的难点问题.传统的面向跨时钟域设计的模型检验方法并没有充分考虑电路特性描述的完整性问题,然而制订完整的电路特性是模型检验有效性的基础,不全面的电路特性描述将可能隐藏设计错误.为生成完整的描述跨时钟域设计的电路特性,本文首先提出基于有限状态自动机的电路特性生成方法;然后为缓解状态空间爆炸问题,提出基于亚稳态的数值化简策略.通过对两个典型的跨时钟域设计进行实验的结果表明,采用本文方法不仅能够达到100%的电路特性覆盖率,而且可以发现被传统方法隐藏的功能错误.同时模型检验的时间代价也能够得到大幅度降低.
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.
出处
《电子学报》
EI
CAS
CSCD
北大核心
2009年第2期258-265,共8页
Acta Electronica Sinica
基金
国家863高技术研究发展计划(No.2006AA010202)
关键词
形式化验证
模型检验
跨时钟域设计
电路特性生成
formal verification
model checking
clock domain crossing design
property generation
