自动测试模式产生(Automatic Test Pattern Generation:ATPG)技术在针对芯片制造缺陷的生产测试中得到广泛应用。ATPG作为测试向量的生成工具,它能根据输入的故障模型,生成简洁、高覆盖率的测试向量(Test Vectors)。但是传统的基于结构化搜索的ATPG算法,如果要提高测试故障覆盖率,需要对电路进行大量的试探性的反复回溯搜索,这样就要耗费大量冗余时间,使得测试成本非常昂贵。而本文提出基于代数公式的二叉判决图和布尔可满足性SAT这两种算法能有效压缩测试时间,它通过将门级电路模块转化为数学逻辑,用求解命题逻辑的代数问题,来达到快速遍历的目的,这样既能解决冗余回溯搜索的时间过长问题,又能提高覆盖率。但对于单纯基于布尔可满足性SAT的算法,由于是以整个变量空间的回溯搜索为基本框架,所以搜索空间很大,时间复杂度较高,会导致算法超时。因为搜索空间越大,就需要越多的回溯搜索时间,特别是对于未知的故障时间将更长。而那些只基于二叉判决图BDD的算法又在构造二叉判决图BDD时可能导致内存溢出等棘手问题,为改善上述缺陷,本文又提出一种不同于遍历式搜索的启发式策略,用增量的方法尽早识别出不可测故障,节省不必要的搜索判定时间。这种二叉判决图BDD与可满足性SAT相混合的一种代数方法,采用布尔差分方程的思想,有效发挥BDD和SAT的各自在时间和空间上的优势,在结点数上做阀值判断,做启发式策略进行算法的互相切换、替代运行。同时避免了在设计BDD时会出现的内存溢出问题和SAT算法超时问题。本研究采用BDD算法的工具开发包CUDD和SAT操作的工具包Zchaff,编写了C++语言代码在基准电路上实现了上述混合算法的仿真验证和应用分析,通过和其他算法的数据对比,发现这种使用智能启发式策略的混合算法比传统的搜索算法或者单一的SAT算法在测试运行时间、回溯次数、故障传递路径、内存占有率上性能都有大幅提升,还能提高ATPG工具生成向量的效率。通过该算法在Tetra MAX工具平台上的实践验证,证明该智能式策略能预先识别冗余故障、不可测故障,又能对难测故障的搜索树进行有效修剪,删除将导致失败的路径和节点赋值模式,使测试生成过程的回溯次数最少,提高了测试生成速度和ATPG的处理效率。最后分析了实验结果和算法的先进性,总结了本人在该算法设计与实现上的主要工作,梳理了算法的创新点和实用性,并对下一步的继续研究工作进行了说明,展望了半导体测试将在系统复杂度、模块间的同步等方面遇到的挑战以及测试技术的研究趋势。