VLSI中形式化的组合电路等价验证方法

摘要

随着集成电路技术的飞速发展,电路的规模也不断增大.电路验证领域正面临前所未有的挑战,如何快速并且完备地完成超大规模集成电路的等价验证,已经成为当前的研究热点.与传统的基于模拟的验证方法相比,形式化的验证方法具有完备性的优点.该文提出的形式化的大规模集成电路中组合电路的等价验证方法主要的创新之处在于:(1)基于层分划的等价配对点生成方法.这方法可以大大提高配对点的命中率,并降低配对点的生成时间,从而大大加快整个验证的速度.(2)基于阈值的错反问题(false negative)回溯控制.有效地选取回溯的时机,控制无效回溯次数,保证计算的效率.(3)基于SAT问题解决框架的子电路分划.将电路的分划、回溯等过程,有机地融入SAT问题DLL算法解决框架之中,避免了反复回溯中的重复计算,并结合SAT问题研究在BCP(Boolean Constrain Propagation)和变量选择方面比较成功的技术,加快验证的速度.此外,我们的验证算法具有很强的灵活性.对于内部,子电路的验证上可以调用不同的SAT Solver来完成;对于外部,可以作为独立的等价电路验证软件使用,也可以作为一个模块被其他算法调用,比如用于时序电路的等价验证.

目录

文摘

英文文摘

第一章绪论

1.1现代集成电路技术的发展

1.2本文的研究背景和内容

1.3国内外研究进展

1.4本文主要贡献

1.5论文的组织结构

第二章SAT问题与等价验证问题简介

2.1 SAT问题简介

2.1.1合取范式的可满足性问题

2.1.2 SAT Solver的发展

2.2等价验证方法介绍

2.2.1基于函数逻辑的方法

2.2.2基于自动测试生成的方法

2.2.3基于以上两种方法的混合

2.3小结

第三章组合电路等价验证的FDCEC方法

3.1引言

3.2组合电路等价验证的FDCEC方法

3.2.1电路的分划过程

3.2.2子电路的验证

3.2.3基于阈值控制的回溯过程

3.3试验结果

3.3.1待测点生成方法的效率的比较

3.3.2错反问题的回溯策略

3.3.3基于层次的划分方法

3.3.4和其他算法的比较

3.4小节

3.5附录

第四章基于SAT问题解决框架的FDCEC方法

4.1引言

4.2 SAT Solver中实现子电路的分划

4.3 SAT Solver中的分支策略

4.4 试验结果

4.5小结

第五章总结和展望

5.1组合电路等价验证工作的总结

5.2今后工作的展望

参考文献

攻读硕士期间撰写的论文

致谢

论文独创性声明及论文使用授权声明