基于BDD和布尔差分的组合电路测试生成方法

在数字系统的测试中, ATPG 是对测试电路产生测试向量的过程[ 1] 。通常ATPG 算法首先给电路插入一个故障; 然后通过在电路输入端激活这个故障, 并将其产生的响应通过电路传播到输出端。若输出信号与无故障电路的期望值不同, 就可以检测到这个故障了。针对组合电路中固定型故障, 目前存在一些ATPG 算法。最基本的是布尔差分法[ 2, 3] 。它描述严格, 是研究组合电路测试生成的理论基础。最经典的是Roth 的D 算法[ 4] , 采用D 立方建立了ATPG 的运算。此外还有Geol 的PODEM算法、Fujiwara 的FAN算法[ 6] 等, 在回溯和加快搜索速度上作出了很大的贡献。Geol 在其PODEM算法[ 5] 中采用二元决策树( binary decision tree, BDT) 进行搜索。Akers[ 7] 提出的使用BDD 来表述逻辑电路则更为实际。近年来, BDD 的理论有了更进一步的完善和发展[ 8, 9] , 并更多地运用到数字电路设计中的验证、综合[ 10] 及自动测试模式生成[ 11] 。本文尝试采用简洁的简化排序二元决策图( reduced orderedBDD, ROBDD) 来对组合电路进行表示及运算; 同时融入布尔差分的思想, 对被测电路BDD 结构进行判断, 从而进行测试生成。

BDD 的相关知识
1. 1 使用BDD 表示布尔函数
根据香农展开式[ 7] , 对于任意一个布尔函数F = f( a, b,c) , 可以将其转换为f( a, b, c) = af( 1, b, c) ∨af( 0, b, c) 。例如对于布尔函数f = ( x1 ∧x2 ) 􊯝 x3 , 可以表示为f = x1 [ ( 1∧x2 ) 􊯝 x3 ] ∨x1 [ ( 0∧x2 ) 􊯝 x3 ] ( 1 )对式( 1) , 将x1 分别设置为0 值和1 值时, 在运算中就会产生两种不同的情况, 以图的形式表述如图1( a) ( 图中的虚线边表示节点变量取0 值, 为节点的左后继; 同理实线边表示取1 值, 为右后继) 所示。接下来继续对此函数中的另外两个变量x2 和x3 也进行同样的展开操作, 直至全部变量都被展开。至此, 布尔函数f = ( x1∧x2 ) 􊯝 x3 中可能的变量取值及运算结果全部由图1( b) 表示。