改进的时间帧展开的时序电路等价验证算法

作     者：丁敏 唐璞山 Ding Min;Tang Pushan

作者机构：上海复旦大学微电子系专用集成电路国家重点实验室上海200433 

基　　金：国家"八六三"高技术研究发展计划(2002AAIZ1460) 国家自然科学基金(90207002) 

出 版 物：《计算机辅助设计与图形学学报》 (Journal of Computer-Aided Design & Computer Graphics)

年 卷 期：2006年第18卷第1期

页      码：53-61页

摘      要：提出一种改进的基于时间帧展开的时序电路等价验证算法,其来源于模型检查中的基于数学归纳的验证算法,在使用并简化了SAT问题中不可满足子集提取过程后,将基本条件检查和归纳检查合并处理.为了能在时间帧展开过程中减少状态搜索空间,利用结构不动点技术并提出了准动态唯一状态约束等改进的方法.实验表明,随着时间帧的不断展开,文中算法运行时间的增长速度明显慢于基于数学归纳法的验证算法,其适合验证经过时序优化后的电路.

主 题 词：时序电路等价验证 形式验证 可满足性问题 

学科分类：080903[080903] 0809[工学-计算机类] 08[工学] 

核心收录：

D　O　I：10.3321/j.issn:1003-9775.2006.01.009

馆 藏 号：203732065...