背景介绍

Combinational ATPG是一个Branch and Bound的演算法，它的本质是在组合电路（Combinational Circuit）内找到适合的输入向量（Input Vector）工具。所有输入讯号的可能组合形成输入空间（Input Space）。这个输入空间的大小主要和组合电路内Primary Inputs的数量有关，它会形成一个二元树（Binary Tree），每个节点（Node）有两个分支（Branch），节点上的符号代表输入讯号的代号，假定左边的分支代表该Node输入值为0，右边的分支代表该Node输入值为1。ATPG用DFS（Depth First Search）可以在输入空间内找到一条路径（Tour），当所有输入讯号（Input）的值依照这条路径输入进去电路设计的时候，能够满足某个我们想观察的性​​质（ Property）。

由于输入空间这个二元树的节点数量太大，需要一个更有效率的资料结构才能够在有限的记忆体空间内表示它；另外一方面人们也致力于发展如何缩小这个输入空间以及更聪明的寻访该输入空间的方法。

随着BDD（Binary Decision Diagram）这类资料结构的提出，人们也应用它来解决ATPG中输入空间过大的问题。其中对于ROBDD（Reduced Order Binary Decision Diagram）除了有着一些时间复杂度不高的运算之外，它有个很好的特点，就是处理的问题如果被处理成ROBDD的格式后，最后简化成相同的ROBDD表示这两个问题是一致的（Canonical），换句话说两个功能相同的电路个别表示成ROBDD的格式时该ROBDD的表示法是唯一的[3]。

《图一 由Binary Tree转化成BDD》

在ATPG中使用BDD技术最主要是运用有​​效的资料结构来在有限的记忆体空间内表示它。运用BDD为ATPG Engine的技术在中小型的电路结构里，它的能力大约可以处理上百个变数的输入空间。但是现今的电路设计已经超过了这个范畴，尤其是把循序电路（Sequential Circuit）考虑进去性质为真否的证明时，BDD往往会面临Memory Explosion的窘境。

组合电路的Solver

将SAT（Satisfiability）problem应用到验证上是90年代有着长足进步的ATPG技术，这方面研究的进步让我们在一个组合电路之中，可以把电路转化成SAT的问题，研究的对象从原来的逻辑电路的推导，简化成在Boolean Domain的Conjunctive Normal Form（CNF）做布林运算（Boolean Operation）[1]。

《图二 基本闸转换成SAT Equations[1]》

这种简化有着什么样的影响？原来使用ATPG要处理的资料结构变简单了，不需要像从前一样从输入讯号端把讯号一层层传送（Propagate）到输出讯号（Output）端。另外把原来的问题转换成CNF后，有一些很有趣的性质被注意到也借此加速了ATPG的运作。

Implication/Unit Clause Rule──SAT问题是一个以上的Clauses组成CNF，亦即POS（Product of Sum），然后求ㄧ组变数的Assignment让整个POS的值为TRUE。当任何一个Clause里面的变数都被分配成FALSE，整个POS的值将会是FALSE。因此当一个Clause里面只剩一个变数没有被分配到值的时候且其他同一个Clause里的变数值都为FALSE，该变数旧的值就马上被决定为TRUE，换句话说即不用寻访该变数为FALSE的分支子树。

《图三 Implication/ Unit Clause Rule[1]》

Conflict Learning──SAT在分配变数的过程中即使运用了Implication依然会遇到分配的变数而让某个Clause产生在该Clause内的所有变数都为FALSE的状况，该情形为产生一个Conflict。直觉的解决方法就是Backtrack回到之前可以分配别的值的变数走另外一条分支。但是其实产生Conflict的时候SAT可以找到一些资讯，而且这些资讯就藏在刚刚那个产生Conflict Clause的变数分配过程之中，我们用下面几张图表示学习（Learning）的过程。

《图四 学习的过程[1]》

Conflict Learning最重要的特点就是，经它学习加入SAT的Conflict Clause只要证明的性质不变，即使经过Backtrack或变数的分配顺序改变这个Conflict Clause依然可以一直被重复使用。

Variable Ordering──一个好的变数分配顺序也会决定整个解SAT问题的效率，因为它直接关系到寻访时的路径。比较(图五)中两棵树的分支情形，发现同样学习到的资讯但是不同的变数分配顺序对于整颗输入空间树删去（Prune）其分支不用寻访的情形也会不同。

《图五 Different Variable Ordering对Search Space的影响[1]》

SAT也有它的一些问题：

第一点即为加入Backtrack的机制，在ATPG找到一组解的时候继续寻访其他的分支；第二点则是仍待研究的问题；至于第三点则是要待有Preimage/Image的观念才能继续解答。

循序电路的Solver

从数学的角度看一个函数y=f(x)，一个合理的x的值可经由该函数对应到一个合理的y的值。所有合理的x值的集合称作Preimage，而所有合理的y值的集合即为Image。

刚刚的观点对应到组合电路，所有合理的输入讯号形成的集合称作Preimage，所有合理的输出讯号形成的集合称做为该电路的Image。但现今使用的晶片大多是被设计成循序电路的样子，下面以一个简单的概念图表达循序电路的组成以及它和组合电路之间的关系，如(图六)所示[2]。

《图六图左为SI、SO、PI、PO、Register；图右为展开的概念》

所以循序电路在多个clock cycles内的行为可以由展开（Unfold）组合电路来描述，原来在组合电路里面输入讯号只有Primary Input，输出讯号只有Primary Output。循序电路里面输入讯号除Primary Input之外还包括上ㄧ个cycle结束时暂存器（Register）的状态，即图六的Pseudo Input；循序电路里面输出讯号除了Primary Output之外也包含这一个cycle里面将要被存入站存器的值，即图六的Pseudo Output。因此在循序电路中Preimage可以看作是在每个clock cycle里面合理的输入讯号形成的集合，而Image是每个clock cycle里面合理的输入讯号形成的集合。

Preimage/Image的重要性在于提供循序电路中验证电路的线索，通常设计者运用模拟（Simulation）电路运作的方式来进行除错与验证的工作，但在电路设计日趋繁琐的今天要完整的运用模拟的方法检查所有可能的输入讯号组合已经不是合理时间内可以完成的。此外，就Assertion来说，如何在一个循序电路内检查一个性质是否在任何时间点恒真，像这类问题光靠模拟已经不能解答。

《图七 循序电路检查Assertion是否成立示意图[4]》

在(图七)表达在一个循序电路中检查一个Assertion是否成立时通常采取的作法。b該性質永遠成立，這時候會在原來的邏輯電路加入一個比較器並且將該比較器的輸出(c)看成是一個Primary Output。"假定这个Assertion希望验证电路里面正常运作情况下ab该性质永远成立，这时候会在原来的逻辑电路加入一个比较器并且将该比较器的输出(c)看成是一个Primary Output。如果能够证明在电路正常运作的情况下形成的Preimage会让c的输出值一直为真（TRUE），这个Assertion就成立了[4]。

希望应用ATPG证明上面的命题，以ATPG的角度来讲，ATPG是一个搜寻合理解的过程，没有办法正面回答在所有输入情况下c的输出值皆为1，但是可以尝试着去找出一个输入讯号的组合让c的输出值为0。如果找到了这种输入讯号的组合，就可以驳斥这个命题；反之，如果找不到这种输入讯号的组合，也可以间接证明上面的命题[6]。

由于现今发展出来的晶片都属于有限状态机（Finite State Machine）， 所以Preimage的大小有限，虽然如此就算只考虑一个cycle内电路输入讯号的所有可能情况，即为其输入空间的大小，假设电路内有50个暂存器与50个Primary Inputs，会得到输入空间的大小为2100。再把如果产生出违反这个性质的结果是经过多个cycle的转换（Transition）考虑进去，这个输入空间又会更大，可以预期如果使用原来用在组合电路的ATPG应用在这问题上，势必要花更多时间和更多记忆体空间。但最重要的是不可能靠无限的展开电路把循序电路的问题转化成组合电路再去给ATPG解。

要解决这个问题，从数学的角度来看如何求x=f(x)中x的所有解集合。首先是从初始的x值开始带入f(x)，来求出x的一个解集合，然后在将此解集合带入f(x)，求出下一个解集合，这样的步骤反覆代入几次之后。最后，会达到一个解集合X，使得X=f(X)，亦即是所谓的fixed point，而这个X就是x=f(x)的所有解集合。

从解循序电路的问题来看，上述的方法就像是从起始的状态（Initial States）经过一个clock cycle来求出下一个时态的状态集合。而将这些状态带入电路，则可以求出下一个时态所有状态的集合。这样子反覆代入之后，最后，可以求出一个状态的fixed point。亦即是由起始状态开始电路可以到达的所有状态的集合（Set of Reachable States）。

想验证的assertion命题会形成一个Image Space，利用求出其Preimage的方法会发现如果Preimage到达fixed point时有和Initial State的集合有交集，就表示这个assertion的性质不成立，反之如果没有交集则成立。也可以试着从Initial State出发如果找到Initial State可以到达的Image的fixed point时，发现该Image有和assertion命题形成的集合有交集，就表示这个assertion的性质不成立，反之如果没有交集则成立[6 ]。

《图八 Preimage和Property形成的Image没有交集的情形 》

传统上人们是使用BDD来寻找Preimage/Image的fixed point，然而使用BDD会有Memory Explosion的问题。因此人们开始使用SAT-based的ATPG演算法并修改让它能够在找到一个解之后Backtrack回来继续找下一个解，直到它找到所有的解为止。

举例来说，下面提出的方法里面，作者修改了原来PODEM的ATPG演算法让它能够应用到循序电路上，此外，这个方法提出一个新概念──Success-driven Learning[5]帮助ATPG删减掉更多输入空间的分支。为了避免表示Preimage/Image时花费太多记忆体，使用BDD来储存它们。

Success-driven Learning和Conflict Learning有什么不同呢？简单来说，Conflict Learning是从Conflict产生的地方学到有用的资讯，而Success-driven Learning是从ATPG结果成功的地方分析出有用的资讯。

Conflict Learning：

Success-driven Learning：

结论

总而言之，近年来ATPG与SAT在解combinational与sequ​​ential上，提出了许多新的演算法（algorithms），人们进一步寻求简化ATPG问题的方法。 Abstraction and Refinement[6]是最新的方向之一。运用原有对Preimage/Image的了解，希望能够把原来的命题先抽象化（Abstraction）成一个比较小的SAT问题，看看该性质在比较小的SAT问题里面有没有解，如果有解表示原来的命题也会有解，如果没有解，再去确定是不是在原来的命题范围里面没有解。如果没有解的结论是FALSE，就进行重新修正（Refinement），希望得到一个更接近原来命题的SAT问题，反覆直到找到解或证明真的没有解为止。

希望ATPG的进步不只在未来能够找到在循序电路内有更有效率的验证方法，另外也希望能够利用更多关于电路上的资讯，提升ATPG Engine朝向Word Level ATPG做更高阶的应用。 （作者为台大电子工程学研究所/台大系统晶片中心研发教授?黄钟扬；研究生林庭豪）

＜参考资料：

[1] Sharad Malik“The Quest for Efficient Boolean Satisfiability Solvers” HTTP://呜呜呜.Princeton.额度/~杀人啊的/

[2] 台湾大学电子所课程 VLSI Testing, 2004

[3] 台湾大学电子所课程 (超大型积体电路)电脑辅助设计系统概论

http://cc.ee.ntu.edu.tw/~ywchang/Courses/EDA/eda.html (HTTP://常常.呃呃.黏土.额度.台湾/~因为常/Courses/EDA/额达.HTML)

[4] 台湾大学电子所课程 系统晶片验证 (SoC Verification)

[5] Efficient preimage computation using a novel success-driven ATPG," Shuo Sheng and Michael S. Hsiao, in Proceedings of the IEEE Design Automation and Test in Europe Conference, March 2003, pp. 822-827.

[6] E. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith, “Counterexample-Guided Abstraction Refinement.” In Proceedings of CAV, pp. 154-169, July 2000.＞

延 伸 阅 读

当IC逐渐演化成内部电路错综复杂的SoC，以往单纯的测试程序也跟着高难度了起来；为了提高这道SoC“健康检查”程序的效率，在前段IC设计中采用可测试性设计（Design for Test ；DFT）技术，成为市场接受度越来越高的解决方案。相关介绍请见「 DFT让SoC“健康检查”更有效率」一文。 近年来由于积体电路制造技术日新月异以及为了缩短电子产品上市时间，单晶片系统的设计技术扮演着举足轻重的地位，其中嵌入式记忆体常用于单晶片系统，因此如何对一嵌入式记忆体作一有效的测试是一个值得重视的问题。 你可在「 半导体记忆体之测试研究」一文中得到进一步的介绍。 在产品日趋轻薄短小，功能日益复杂的前提下，朝高整合度的系统单晶片（System on Chip；SoC）发展之途，已成为未来半导体产业演进的终极目标。由于SoC的系统设计整合了多项不同功能的电路在相同的IC上，测试上也不同于以往将单功能的IC个别测试后，即可组成系统；取而代之的是高复杂度的SoC测试技术。在「IC测试技术探索」一文为你做了相关的评析。

市场动态

Mentor Graphics宣布其行业领先的自动测试向量生成工具（ATPG）、FastScan以及它的嵌入式确定性测试工具TestKompress新增加自动化处理功能——ATPG Expert。 ATPG Expert功能部件能对设计进行自动分析，并智慧化地使用ATPG工具（Fastscan和Testkompress）所提供的命令处理测试向量生成中的所有复杂性，如RAM的Shadow logic和汇流排冲突问题。你可参考 「Mentor Graphics宣布FastScan和TestKompress测试设计工具增强自动化处理功能，取得最佳的测试覆盖成果」一文。 SynTest宣布推出DFT-PRO 100和200系列入门级ATPG (Automatic Test Pattern Generation)套装软体，该套装软体包括用于复杂ASIC测试的基本DFT (Design-for-Test)工具，这些工具可对已插入扫描链的网表进行作业，其中包括具有以下用途的工具：测试DFT规则违反、自动测试向量生成(ATPG)和测试向量格式转换以便和Advantest、Agilent、Credence及Teradyne等供应商的ATE相容。 你可在「SynTest发布ATPG入门级套装软体可提高ASIC设计品质」一文中得到进一步的介绍。 以往的系统设计是将CPU，DSP，PLL，ADC，DAC或Memory等电路设计成IC后，再加以组合变成完整的系统，但现今的设计方式是将上述的电路直接设计在同一个IC上，或购买不同厂商的IP（intellectual property），直接加以整合，此方式称为系统单晶片（SoC)设计方法。 SoC方式降低设计和制造成本，但对于测试来说却变得更为复杂，测试成本也越来越高，测试问题已不容忽视。在「SOC晶片设计与测试」一文为你做了相关的评析。