基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究

发布时间：2021-10-08 06:24

　　近些年在布尔可满足性（SAT）领域取得了较大进展,一系列基于DPLL框架的优化算法被提出,有效SAT解算器诸如zChaff等已可解决很大规模的SAT问题。SAT作为一个优秀引擎在EDA领域已广泛应用,本论文的主要方向就是探索如何有效地将SAT技术应用于等价性验证和测试生成这两类重要问题中。下面概括本论文的主要研究方向和创新点:1.基于输出分组和电路SAT的组合等价性验证技术。随着芯片设计规模日益庞大复杂,功能验证成为现阶段IC设计过程中的瓶颈环节,而传统模拟技术已很难满足现时集成电路设计的要求。作为模拟技术的补充,组合等价性验证工具在IC功能验证中使用已日益普遍。本文提出一种基于电路可满足性和输出分组技术的组合电路等价性验证算法。算法首先使用与非图结构哈希技术来简化验证任务。对那些具有较多输出的复杂电路,为共享结构信息从而提高验证速度,使用输出分组技术将那些共享较多内部结点的输出转化为一个子问题,从而验证问题可转化为一系列验证子问题。对每一个子问题,使用将电路SAT和BDD学习等技术结合的验证算法来解决。实验结果表明该类方法可有效用于解决大规模电路的验证问题。2.结合不变量提取和时序S... 

【文章来源】：浙江大学浙江省 211工程院校 985工程院校 教育部直属院校

【文章页数】：124 页

【学位级别】：博士

【部分图文】：

IC设计流程中的等价性验证

匹配时间比较结果

5832这12个电路，两种方法算法均能在0.1秒内完成匹配，故这里只给出:1423到538584共10个测试电路的比较结果。图4一5匹配时间比较结果图4一5中给出文献【571和本文算法匹配所用的CPU时间(单位为S)。图4一6

【参考文献】：
期刊论文
[1]基于切割法的时序电路等价验证[J]. 黄伟,唐璞山.  复旦学报(自然科学版). 2006(01)
[2]改进的时间帧展开的时序电路等价验证算法[J]. 丁敏,唐璞山.  计算机辅助设计与图形学学报. 2006(01)
[3]使用输出分组和电路可满足性的等价性验证算法[J]. 郑飞君,严晓浪,葛海通,杨军,卢永江.  计算机辅助设计与图形学学报. 2005(11)
[4]基于增量可满足性的等价性检验方法[J]. 李光辉,李晓维.  计算机学报. 2004(10)
[5]结合二叉判决图和布尔可满足性的等价性验证算法[J]. 严晓浪,郑飞君,葛海通,杨军.  电子学报. 2004(08)



本文编号：3423592