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

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

Property Generation Method for Model Checking on Clock Domain Crossing Design

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 metastabi...