[摘要]现代数字集成电路技术的飞速发展，对计算机辅助测试提出更多更高的要求，可满足性方法（SAT-Satisfiability）作为一种有效的完备测试生成方法，近年来在集成电路测试领域引起广泛的研究兴趣，并取得了一些应用上的成功。对电子数字电路的SAT可满足性算法进行研究，希望能够有助于提升我们对相关问题的认识，以有助于数字电路测试的不断发展和进步。
[关键词]数字电路 SAT可满足性测试 公式可满足性 可满足性搜索问题
中图分类号：TN7文献标识码：A 文章编号：1671－7597（2008）0410017－01
随着近年来数字电路应用的不断增加，对数字电路进行测试日益成为一项经常性的行为。对于大规模和超大规模集成电路，依靠人力来测试故障已不可能，必须利用计算机生成和执行测试，数字电路可满足性测试方法是数字电路测试的一种有效方法。
一、数字电路测试其他基本算法
测试生成算法就是针对具体的目标故障f产生一个测试模式t，将该模式用作输入以激活电路的故障，并在可观测点观测其行为是否与无故障电路的行为有区别。若不相同的话，就说该测试模式t检测了该目标故障f。这其中包括了两层含意：在故障点产生一个差错信号；传播该差错信号到原始输出端。一般测试算法常见的有：穷举方法：测试生成的目的就是要查找一个具有最大故障覆盖率的测试集合。测试生成最简单的方法就是穷尽真值表方法。见图1。
图1
代数方法：代数方法（也指布尔差分法，它是组合电路测试生成的一种方法。它使用布尔方程来描述电路，它的描述严格而简洁，物理意义清晰。因此在研究组合电路测试生成的理论和方法时具有重要的意义。结构化方法：
结构化方法是以网络的拓扑结构为出发点的各种测试产生算法。在这种方法中，它不直接化简布尔方程，而是用一定的数据结构来表示电路。即电路的功能由网表和模块库联合描述，网表描述电路的拓扑结构以及模块的类型，而库则提供了每个类型模块所实现的逻辑函数。它对输入信号值的各种可能组合进行枚举，采用分支界定法得到符合条件的输入数据。这实际上是一种回溯搜索算法。在此类算法中，人们采用各种各样的分析类型来加速基本的分支界定方法的搜索过程。测试生成算法框；基于SAT的方法，基于布尔可满足性SAT方法用单一的布尔公式来描述电路的逻辑功能，其公式大多采用合取范式CNF表示。下面我们将对数字电路SAT可满足性算法进行详细介绍。
二、数字电路SAT可满足性算法研究
（一）公式可满足性问题
公式可满足性指判断公式是否可满足和找出相应的满足赋值。从空赋值开始，回溯搜索算法遍历赋值空间，在搜索过程中，一直保留着一棵判决树，判决树中的节点选择一个值给未赋值的变量，这样的赋值作为判断赋值，判断级与判决树中赋值的深度相联系，判决树根的第一次判断赋值称着判断级。
（二）可满足性问题的搜索算法
可满足性问题的搜索算法作为搜索算法库，因而可集成为其它应用程序的搜索。搜索过程的每一阶段称为判断级，假定初始子句数据库lp、初始赋值A和判断0级，可以为空的初始赋值看着附加的约束问题，使搜索限制于维布尔空间，娜 A随搜索进行着修改。递归搜索过程由以下四个主要运行组成：
DecideQ，在搜索过程的每阶段选择判断赋值，判断过程一般基于启发示信息；
Deduce（），执行布尔约束传播，合成蕴涵图，此过程等价于数字电路蕴涵式的推导；Diagnose（），识别产生矛盾的原因和用蕴涵添加子句库，这些归为矛盾子句:Erase（），删去当前判断级赋值。
参考文献：
[1]刘歆、熊有伦，《数字电路测试生成的基本算法》，载《微电子学与计算机》2002，（2）.
[2]沈茜，《数字电路测试的故障诊断和测试码生成》，载《科技资讯》2007，（34）.
[3]王宇、陈宇，《数字电路测试生成中的几种仿生优化算法》，载《信息技术》2007，（9）.
[4]郭希维、苏群星、谷宏强，《数字电路测试中的关键技术研究》，载《科学技术与工程》2006，（18）.
[5]胡小波，《数字电路自动测试系统研究》，载《江汉大学学报（自然科学版）》35.（2）.