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

摘要：

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

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

所属期刊栏目：18

分类号：TN47(微电子学、集成电路（IC）)

资助基金：国家科技攻关项目2002AAIZ1460;中国科学院资助项目90207002

在线出版日期：2006-03-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：53-61