基于BDD的逻辑电路验证

发布时间：2023-10-04 02:17

　　VLSI技术的快速提高导致硬件设计复杂性增大,使得检查电路的正确性已经变成一项非常困难的任务。在后面的设计环节中或者等到产品完成后再纠正错误将会耗费更多的费用,因此,为了能避免高额的产品开发费用,设计中的早期错误检测变得越来越重要。 传统的验证方法就是对设计进行穷尽的模拟,即建立一个模型,用软件或者硬件方法赋予输入大量的测试向量,然后把模型输出和参考模型的功能进行比较来达到验证目的。但是这种方法不能完全保证设计的正确性,尤其是在大规模电路设计中,模拟验证的时间更要花费几年之久,这是我们无法忍受的。作为传统的模拟验证方法的补充,形式验证越来越引起人们的关注,它是通过严格的数学推理来证明一个系统满足全部或部分规范。形式化验证能大大减小设计时间而且能对设计进行完全覆盖验证。它不用波形或者激励而是直接采用硬件描述的方式,这样能更快得到结果和探测错误。等价性验证作为形式验证方法的一种,常被用于验证综合后电路以及人工修改后的电路。等价性检查主要用于验证RTL和RTL之间,RTL和门级网表之间以及门级网表和门级网表之间的等价性。 本论文对一些传统的组合电路及时序电路等价性验证方法进行了介绍、分析、比...

【文章页数】：61 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
引言
1 绪论
    1.1 研究的背景和意义
    1.2 国内外研究现状
2 集成电路设计验证综述
    2.1 模拟验证方法
        2.1.1 软件模拟
        2.1.2 硬件仿真
        2.1.3 测试
    2.2 形式化验证
        2.2.1 模型检验
        2.2.2 定理证明
        2.2.3 等价性检查
    2.3 半形式化验证
        2.3.1 覆盖率驱动的验证方法
        2.3.2 符号模拟
    2.4 本章小结
3 二叉判定图及其在等价性验证中的应用
    3.1 二叉判定图相关的定义
        3.1.1 基本的二叉判定图
        3.1.2 有序二叉判定图
        3.1.3 精简的有序二叉判定图
    3.2 二叉判定图的性质
    3.3 电路的二叉判定图表示
    3.4 二叉判定图的运算
        3.4.1 二叉判定图的迭代运算
    3.5 二叉判定图的变量排序
        3.5.1 变量排序对二叉判定图的影响
        3.5.2 深度优先BDD 构造算法
        3.5.3 动态变量排序
    3.6 本章小结
4 基于BDD 的组合电路等价性验证
    4.1 随机仿真
    4.2 基于替代的结构性验证方法
    4.3 割集和局部BDD 技术
    4.4 建议的算法和实验结果分析
    4.5 本章小结
5 基于BDD 的时序电路等价性验证
    5.1 基于状态遍历的时序等价性验证
    5.2 时序电路随机仿真
    5.3 时序电路结构相似性技术
    5.4 建议算法的验证流程
    5.5 建议算法实验结果及分析
    5.6 本章小结
6 工作总结与展望
    6.1 工作总结
    6.2 工作展望
参考文献
在学研究成果
致谢



本文编号：3851115