結(jié)合邏輯模擬和布爾可滿足性的設(shè)計(jì)錯(cuò)誤診斷方法

摘 要:在集成電路設(shè)計(jì)驗(yàn)證與調(diào)試過(guò)程中，邏輯錯(cuò)誤診斷工具通常會(huì)給出一定數(shù)量的候選錯(cuò)誤區(qū)域，然后通過(guò)特定的算法盡可能多地減少候選區(qū)域，以方便錯(cuò)誤的準(zhǔn)確定位。在此提出一種結(jié)合模擬與布爾可滿足性(SAT)的錯(cuò)誤診斷方法，用于提高錯(cuò)誤診斷準(zhǔn)確性。該方法首先使用模擬方法對(duì)候選的錯(cuò)誤區(qū)域逐一進(jìn)行判斷，對(duì)于不能由模擬方法判別的候選區(qū)域，使用基于SAT的形式化方法進(jìn)一步判斷。針對(duì)ISCAS′85電路的實(shí)驗(yàn)結(jié)果表明，該方法具有較高的錯(cuò)誤診斷準(zhǔn)確性和效率。

關(guān)鍵詞:設(shè)計(jì)驗(yàn)證;錯(cuò)誤診斷;布爾可滿足性;邏輯模擬

中圖分類號(hào):TN710文獻(xiàn)標(biāo)識(shí)碼:A

文章編號(hào):1004-373X(2010)06-022-04

Error Diagnosis of Logic Simulation and Boolean Satisfiability

ZENG Songwei，LI Guanghui

(School of Information Engineering，Zhejiang Forestry University，Lin′an，311300，China)

Abstract:In the integrated circuit design verification and debugging process，the diagnosis tools often present some candidate errorneous logic zones，and then reduce these zones as many as possible with special algorithms so that the designers can locate the error conveniently.A novel method integrating logic simulation and Boolean satisfiablity (SAT) for improving the accuracy of design error diagnosis.This method uses logic simulation to decide each candidate zone at first，and then a SAT solver is called to deal with those zones which can′t be decided by logic simulation.Experimental results on ISCAS′85 benchmark circuits show the efficiency and precision of the presented method.

Keywords:design verification;error diagnosis;Boolean satisfiability;logic simulation

0 引 言

在集成電路設(shè)計(jì)流程中，經(jīng)常發(fā)生設(shè)計(jì)規(guī)范與設(shè)計(jì)實(shí)現(xiàn)不一致的情況。當(dāng)驗(yàn)證工具發(fā)現(xiàn)這種情況時(shí)，必須進(jìn)行設(shè)計(jì)錯(cuò)誤診斷，即識(shí)別或盡可能地縮小設(shè)計(jì)實(shí)現(xiàn)中可疑的錯(cuò)誤區(qū)域，以利于隨后進(jìn)行的錯(cuò)誤糾正。現(xiàn)有的錯(cuò)誤診斷方法可以分為兩大類:基于錯(cuò)誤模型的診斷方法和無(wú)錯(cuò)誤模型的診斷方法。如果按照診斷推理方法來(lái)分，則可分為基于模擬的診斷方法和符號(hào)(形式化)診斷方法。基于模擬的錯(cuò)誤診斷方法依賴于許多可以區(qū)分規(guī)范與實(shí)現(xiàn)的測(cè)試向量，這些向量可以是隨機(jī)產(chǎn)生的向量，門級(jí)故障測(cè)試向量，也可以是等價(jià)性檢驗(yàn)工具產(chǎn)生的區(qū)分向量。根據(jù)這些向量的模擬結(jié)果，候選的錯(cuò)誤區(qū)域被逐步地減小或壓縮。盡管基于模擬的方法不夠準(zhǔn)確，但它處理能力很強(qiáng)，非常適于大型設(shè)計(jì)的診斷。大多數(shù)符號(hào)方法是基于二叉判決圖(BDD)的算法，這類方法試圖發(fā)現(xiàn)那些最有可能導(dǎo)致輸出錯(cuò)誤的電路信號(hào)，通過(guò)對(duì)這些信號(hào)的再綜合(Re-Synthesis)可以糾正整個(gè)實(shí)現(xiàn)中的錯(cuò)誤。然而，基于BDD的算法可能會(huì)導(dǎo)致內(nèi)存爆炸，因而處理能力有限。Shi-Yu Huang [4]提出一種基于故障模擬的錯(cuò)誤診斷方法。這種方法比基于模擬的方法更準(zhǔn)確，但計(jì)算復(fù)雜性又遠(yuǎn)低于基于BDD的符號(hào)化方法，而且可以推廣到含多個(gè)錯(cuò)誤的時(shí)序電路錯(cuò)誤診斷。近年來(lái)，由于可滿足性算法的研究進(jìn)展，有人提出基于SAT的錯(cuò)誤診斷算法，如Jain [2]， Veneris[5]都在這方面做出了很好的嘗試。SAT的應(yīng)用現(xiàn)在正被廣泛地應(yīng)用到各種EDA領(lǐng)域，如邏輯綜合、測(cè)試生成、等價(jià)性檢驗(yàn)和屬性檢驗(yàn)等方面，將SAT應(yīng)用到設(shè)計(jì)錯(cuò)誤診斷無(wú)疑具有很大的研究潛力。針對(duì)電路設(shè)計(jì)中存在未知約束的情形，Jain提出了兩種驗(yàn)證和錯(cuò)誤診斷的方法:一是將未知約束的模型結(jié)合到SAT解答器中;二是利用通過(guò)修改電路結(jié)構(gòu)來(lái)構(gòu)建未知約束的模型。在此基礎(chǔ)上，對(duì)候選的(錯(cuò)誤源)進(jìn)行淘汰，從而提高錯(cuò)誤診斷的準(zhǔn)確性。

本文考慮對(duì)于給定的候選錯(cuò)誤區(qū)域集合，如何盡可能減少錯(cuò)誤區(qū)域，使得錯(cuò)誤糾正更有針對(duì)性，從而提高錯(cuò)誤診斷的準(zhǔn)確性。提出了一種結(jié)合邏輯模擬和SAT的方法，用于提高邏輯設(shè)計(jì)錯(cuò)誤診斷的準(zhǔn)確性。該方法使用門級(jí)電路的固定型故障測(cè)試向量而不是隨機(jī)向量進(jìn)行模擬，能夠快速檢測(cè)大量的設(shè)計(jì)錯(cuò)誤。然后，使用基于SAT的布爾比較進(jìn)一步增強(qiáng)邏輯模擬。針對(duì)ISCAS′85電路的實(shí)驗(yàn)結(jié)果表明，提出的方法能夠有效改善邏輯錯(cuò)誤診斷的準(zhǔn)確性。

1 基于區(qū)域的錯(cuò)誤模型

Boppana提出一種基于模擬與區(qū)域錯(cuò)誤模型的診斷方法，這種方法不需要具體的錯(cuò)誤模型，將可能的錯(cuò)誤區(qū)域的所有輸出值置為X值(稱該區(qū)域?yàn)閄表)，從而反映出錯(cuò)誤的隨機(jī)性和任意性。然后通過(guò)測(cè)試向量的模擬來(lái)逐步減少候選區(qū)域，提高錯(cuò)誤診斷的準(zhǔn)確性。下面簡(jiǎn)要介紹該方法的思想。

定義1(X表) 如果在模擬過(guò)程中，電路中的某個(gè)信號(hào)集合中元素的值設(shè)置為X，并且通過(guò)三值模擬傳播到受其影響的邏輯，那么這個(gè)集合稱為X表。

定義2(基于區(qū)域的錯(cuò)誤) 一個(gè)錯(cuò)誤稱為基于以r為半徑，以結(jié)點(diǎn)p為中心的區(qū)域錯(cuò)誤，如果集合E={e1，e2，…，ek}中元素的邏輯函數(shù)是錯(cuò)誤的，并且滿足下列條件:

l(wèi)，1≤l≤k，dis(el，p)≤r

其中:dis(el，p)是指從結(jié)點(diǎn)el到達(dá)結(jié)點(diǎn)p的最短路徑長(zhǎng)度。

Boppana[6]假設(shè)實(shí)現(xiàn)電路中的所有錯(cuò)誤全部包含在至少一個(gè)候選區(qū)域中，那么如果某個(gè)區(qū)域的外部發(fā)現(xiàn)有錯(cuò)誤，則該區(qū)域可以從候選表中刪除。圖1描述了基于X表的診斷方法，圖中黑色填充的區(qū)域表示候選的錯(cuò)誤區(qū)域，IN表示輸入向量。在左下圖中，對(duì)于輸入IN，設(shè)計(jì)規(guī)范與實(shí)現(xiàn)的輸入分別為0和X，說(shuō)明該候選區(qū)域可能包含錯(cuò)誤，所以不能從候選列表中刪去。從右下圖可以發(fā)現(xiàn)，對(duì)于輸入IN，設(shè)計(jì)規(guī)范與實(shí)現(xiàn)的輸入分別為0和1，說(shuō)明在該候選區(qū)域外部還存在錯(cuò)誤，即它不能包含所有錯(cuò)誤，所以將從候選列表中被刪除。

圖1 基于模擬與區(qū)域模型的錯(cuò)誤診斷方法

在Boppana的模擬算法中，由于使用了X值表示任意的功能，顯然會(huì)導(dǎo)致邏輯運(yùn)算結(jié)果的不準(zhǔn)確，并可能屏蔽某些錯(cuò)誤。因此，本文考慮在模擬過(guò)程之后，再使用形式化的方法對(duì)剩余的錯(cuò)誤源區(qū)域過(guò)濾，以提高設(shè)計(jì)錯(cuò)誤診斷方法的準(zhǔn)確性。此外，本文提出的算法仍然以Boppana的假設(shè)為前提，即假定實(shí)現(xiàn)電路中的錯(cuò)誤全部包含在至少一個(gè)候選區(qū)域內(nèi)。對(duì)于單錯(cuò)誤情形，上述假設(shè)顯然總是成立的。對(duì)于多個(gè)錯(cuò)誤的情形，如果給定的區(qū)域足夠大，由于大多數(shù)錯(cuò)誤或故障是局部性的，上述假設(shè)仍然能夠滿足。

2 結(jié)合模擬和SAT的設(shè)計(jì)錯(cuò)誤診斷方法

根據(jù)上面的分析，首先要找到一個(gè)輸入向量(區(qū)分向量)，使得設(shè)計(jì)規(guī)范與設(shè)計(jì)實(shí)現(xiàn)的輸出響應(yīng)不同。為了提高發(fā)現(xiàn)錯(cuò)誤的效率，使用門級(jí)電路的固定型故障測(cè)試集進(jìn)行模擬，并用基于SAT的布爾比較增強(qiáng)模擬效果。

2.1 并行邏輯模擬算法

為便于表示未知信號(hào)(即X值)，本文使用兩個(gè)布爾變量來(lái)編碼每個(gè)信號(hào)值 [2]。表1列出編碼方案;表2給出基本門的求值運(yùn)算法則，這里A = (A1，A2)，B=(B1，B2)表示門的兩個(gè)輸入，符號(hào)∧和∨分別表示與運(yùn)算符以及或運(yùn)算符。表2中對(duì)應(yīng)與/或運(yùn)算的第二、三列分別表示門輸出W的第一位編碼W1與第二位編碼W2。但其中的非運(yùn)算僅以A的非運(yùn)算為例，其結(jié)果是通過(guò)交換它的兩位編碼得到。為了提高算法的效率，使用并行的邏輯模擬[8]，這時(shí)用兩個(gè)32位的機(jī)器字來(lái)表示每個(gè)電路結(jié)點(diǎn)的邏輯值，兩個(gè)機(jī)器字中相同的位對(duì)應(yīng)于某個(gè)向量響應(yīng)值的兩個(gè)編碼。

表1 邏輯模擬中信號(hào)編碼方案

W1W2W

010

101

11X

表2 邏輯模擬的運(yùn)算法則

運(yùn)算類型W1W2

A∧BA1 ∧ B1A2∨B2

A∨BA1∨B1A2 ∧B2

-AA2A1

2.2 基于SAT的布爾比較算法

定義3(布爾可滿足性問(wèn)題，簡(jiǎn)記為SAT) 給定一個(gè)布爾函數(shù)f:Bn→B，這里B = {0，1}，布爾可滿足性問(wèn)題是指找到一組變量賦值X*，使得f (X*) = 1，或者證明不存在這樣的變量賦值。

如果布爾函數(shù)f存在變量賦值X*，使得f (X*) =1，那么稱f是可滿足的;如果不存在這樣的變量賦值，則稱f為不可滿足的。給定一個(gè)組合電路，電路可滿足性問(wèn)題是指判定是否存在一組原始輸入賦值使得至少一個(gè)原始輸出的值為1。如果存在這樣的賦值，則稱之為電路的滿足賦值[9]。

大多數(shù)SAT程序都用合取范式(Conjunctive Normal Form，CNF) 公式表示布爾函數(shù)。

為了進(jìn)一步增強(qiáng)模擬算法，在此提出一種基于SAT的布爾比較方法。類似Jain[2]提出的策略，為了構(gòu)造布爾比較的miter結(jié)構(gòu)的CNF公式，所有受候選區(qū)域輸出影響的信號(hào)的編碼方案仍然與表1給出的方案相同。如果兩個(gè)電路信號(hào)值均為確定的布爾值0或1時(shí)，按照通常的運(yùn)算規(guī)則作邏輯運(yùn)算;如果其中某個(gè)信號(hào)為X值時(shí)，其相應(yīng)的邏輯運(yùn)算方案如下:

X∧1=X，X∨1=1;X0=0，X∨0 =X

以圖2(a)所示的與門為例，假設(shè)信號(hào)a為X，而信號(hào)b只有兩種可能的取值0與1，那么輸出信號(hào)G受未知信號(hào)a的影響。這時(shí)可以如圖2(b)所示，使用兩個(gè)布爾變量(a0，a1)表示a，(g0，g1)表示G。該與門的所有可能的賦值情況有以下6種:

X∧1=X，X∧0=0，1∧1=1，1∧0=0，

0∧1=0，0∧0=0

式中:后兩種賦值可合并為:(a = 0) →(G = 0)，將上述真值表轉(zhuǎn)化成相應(yīng)的CNF公式如下:

(┐a0+ a1+┐b + g0) (┐a0+ a1+┐b +┐g1)

(┐a0+ a1+b+┐g0) (┐a0+a1+b+g1)

(a0+┐a1+┐b +┐g0) (a0+┐a1+┐b +g1)

(a0+┐a1+ b +┐g0) (a0+┐a1+b+g1)

(┐a0+┐a1+┐b +g0)(┐a0+┐a1+┐b + g1)

(┐a0+┐a1+b+┐g0)(┐a0+┐a1+ b+g1)

圖2 含有未知約束的與門編碼方案

下面可以給出基于SAT的錯(cuò)誤診斷方法:

(1) 如圖3所示，將實(shí)現(xiàn)電路與規(guī)范電路中的對(duì)應(yīng)原始輸入聯(lián)接到一起，將對(duì)應(yīng)的原始輸出聯(lián)接到一個(gè)異或門，建立布爾比較的miter結(jié)構(gòu)[10];

圖3 布爾比較的miter結(jié)構(gòu)

(2) 將每個(gè)受未知約束影響的信號(hào)用兩個(gè)新的布爾變量編碼;

(3) 構(gòu)造miter的CNF公式;

(4) 使用SAT程序求解上述CNF公式。

接下來(lái)，描述提出的設(shè)計(jì)錯(cuò)誤診斷算法。該算法每次處理一個(gè)候選錯(cuò)誤區(qū)域。設(shè)spec表示完整的設(shè)計(jì)規(guī)范;impl表示含有候選錯(cuò)誤區(qū)域的實(shí)現(xiàn);數(shù)組Z表示候選錯(cuò)誤區(qū)域的所有輸出，那么結(jié)合邏輯模擬與SAT的診斷算法如下:

Diagnosis(spec，impl，Z)

{

result = TRUE;

XSim(spec，impl，Z，n);// 邏輯模擬，n表示模擬的向量個(gè)數(shù)

for each primary output

{

result = Match(X-response，Correct response);//比較規(guī)范與實(shí)現(xiàn)的響應(yīng)

if(result = = FALSE)

return (result);

}

result = Verify_SAT(spec，impl，Z);

return (result);

}

在上述算法中，函數(shù)Xsim用于帶X值的邏輯模擬，首先對(duì)規(guī)范電路并行模擬n 個(gè)測(cè)試向量。然后使用相同的n 個(gè)向量并行模擬含候選錯(cuò)誤區(qū)域的實(shí)現(xiàn)電路，此時(shí)要將候選區(qū)域的所有輸出信號(hào)設(shè)置為X值。在比較規(guī)范電路和實(shí)現(xiàn)電路的響應(yīng)字時(shí)，只有當(dāng)某個(gè)向量使得某兩個(gè)對(duì)應(yīng)的原始輸出信號(hào)分別是0(1)和1(0)，才表明檢測(cè)到實(shí)現(xiàn)電路中候選區(qū)域外部的錯(cuò)誤，此時(shí)算法結(jié)束，不必再調(diào)用SAT程序Verify_SAT。如果模擬算法不能檢測(cè)到錯(cuò)誤，則調(diào)用SAT程序繼續(xù)驗(yàn)證。當(dāng)SAT程序的返回值為FALSE(可滿足)時(shí)，表示算法檢測(cè)到了實(shí)現(xiàn)電路中的錯(cuò)誤。當(dāng)SAT程序的返回值為TRUE(不可滿足)時(shí)，表示算法沒(méi)有檢測(cè)到實(shí)現(xiàn)電路中的錯(cuò)誤。當(dāng)上述算法發(fā)現(xiàn)實(shí)現(xiàn)電路中有錯(cuò)誤時(shí)，候選錯(cuò)誤區(qū)域可以剔除，但沒(méi)有發(fā)現(xiàn)錯(cuò)誤時(shí)則要保留候選區(qū)域。

3 實(shí)驗(yàn)結(jié)果及其分析

這里使用C++語(yǔ)言實(shí)現(xiàn)了提出的錯(cuò)誤診斷方法，并調(diào)用普林斯頓大學(xué)的SAT程序包Zchaff完成實(shí)驗(yàn)中的布爾比較。實(shí)驗(yàn)環(huán)境是:P4 1.4 GHz的PC機(jī)，256 MB內(nèi)存，操作系統(tǒng)為Mandrake Linux 8.1。第一組實(shí)驗(yàn)是用來(lái)證明本文方法提高錯(cuò)誤診斷算法效率的能力。第二組實(shí)驗(yàn)主要用于研究算法性能隨著錯(cuò)誤區(qū)域大小變化的規(guī)律。因?yàn)榕c參考文獻(xiàn)中實(shí)驗(yàn)環(huán)境有所不同，根據(jù)體系結(jié)構(gòu)的差異以及性能評(píng)測(cè)標(biāo)準(zhǔn)，對(duì)來(lái)自原文中的原始數(shù)據(jù)做了相應(yīng)的換算。

3.1 提高錯(cuò)誤診斷算法效率的實(shí)驗(yàn)

在這個(gè)實(shí)驗(yàn)里，僅考慮存在單錯(cuò)誤的情形。以ISCAS′85電路作為設(shè)計(jì)規(guī)范，通過(guò)在電路中隨機(jī)注入一個(gè)門置換錯(cuò)誤得到實(shí)現(xiàn)電路，并隨機(jī)地選擇半徑為1或2的候選錯(cuò)誤區(qū)域。表3給出了所得的實(shí)驗(yàn)結(jié)果，并與Jain[2]的結(jié)果(實(shí)驗(yàn)環(huán)境:Sun Ultra360，512 MB內(nèi)存)進(jìn)行比較。表3中第一列是電路名，第二列表示候選區(qū)域個(gè)數(shù)，第三列給出了邏輯模擬的測(cè)試向量個(gè)數(shù)，第四列和第五列分別給出本文提出的方法與Jain的算法最后得到的候選區(qū)域個(gè)數(shù)，第六列和第七列分別表示兩種算法所需要的運(yùn)行時(shí)間。Jain的算法沒(méi)有能夠完成C3540電路的錯(cuò)誤診斷。從表3可以看出，本文方法所花費(fèi)的運(yùn)行時(shí)間比Jain的算法要少，對(duì)電路平均要快一個(gè)數(shù)量級(jí)。因?yàn)槭褂秒娐返臏y(cè)試集可以較快地發(fā)現(xiàn)錯(cuò)誤，從而避免多次調(diào)用SAT程序，導(dǎo)致總的算法時(shí)間的減少。事實(shí)上，布爾比較時(shí)間遠(yuǎn)遠(yuǎn)多于模擬算法所需的時(shí)間。此外，本文方法減少的候選區(qū)域數(shù)比Jain的算法要多，說(shuō)明診斷的準(zhǔn)確性更高。

表3 錯(cuò)誤診斷的時(shí)間

電路候選區(qū)域數(shù) 向量數(shù)

真正的候選區(qū)域數(shù)

本文方法Jain的方法

時(shí)間 /s

本文方法Jain的方法

C4321046250.040.74

C4991058450.1614.39

C8801067350.071.16

C13551098350.137.65

C19081088550.7045.77

C26709119450.6425.35

C3540101894-2.77-

C53155210550.7050.17

C628810125501.111.84

C75529293450.8227.36

3.2 錯(cuò)誤區(qū)域大小對(duì)算法性能的影響

這個(gè)實(shí)驗(yàn)主要用于錯(cuò)誤區(qū)域大小對(duì)于診斷算法性能、準(zhǔn)確性的影響。對(duì)每個(gè)實(shí)驗(yàn)電路，隨機(jī)注入一個(gè)門置換錯(cuò)誤，并選擇10個(gè)任意的候選區(qū)域，分別考察區(qū)域半徑radius為0，1，2時(shí)的三種情況。表4給出了在不同條件下診斷算法所需的時(shí)間。從這個(gè)表列出的實(shí)驗(yàn)結(jié)果來(lái)看，隨著錯(cuò)誤區(qū)域的增大，算法的運(yùn)行時(shí)間增大，而且診斷的準(zhǔn)確性有所下降。實(shí)際上，錯(cuò)誤區(qū)域的增大對(duì)模擬算法的影響不大，然而基于SAT的布爾比較，則會(huì)受到較大的影響，主要是因?yàn)橄鄳?yīng)的CNF公式規(guī)模通常會(huì)變大，從而導(dǎo)致SAT程序的搜索空間可能變大，其回溯次數(shù)將要增加。

表4 錯(cuò)誤區(qū)域大小對(duì)算法運(yùn)行時(shí)間、準(zhǔn)確性的影響

電路

radius=0

Cand.TrueTime

radius=1

Cand.TrueTime

radius=2

Cand.TrueTime

C4321000.011020.05

1030.07

C4991030.311040.331060.35

C8801030.061040.071030.11

C13551030.201030.211030.19

C19081030.271040.271040.29

C26701030.301040.381050.64

C35401031.821051.051042.72

C53151030.591030.451030.72

C62881040.581040.961052.79

C75521030.681040.771071.15

4 結(jié) 語(yǔ)

伴隨著驗(yàn)證的一個(gè)重要問(wèn)題是設(shè)計(jì)錯(cuò)誤的診斷和糾正。通常，診斷工具會(huì)給出一定數(shù)量的錯(cuò)誤源區(qū)域，然后使用某種算法去壓縮這些區(qū)域，使得可疑的區(qū)域盡可能地小，從而方便設(shè)計(jì)錯(cuò)誤的定位。本文提出一種結(jié)合模擬與布爾可滿足性的錯(cuò)誤診斷方法，用于提高錯(cuò)誤診斷準(zhǔn)確性。該方法首先使用模擬方法盡可能多地淘汰假的錯(cuò)誤源區(qū)域，對(duì)于不能由模擬方法判別的候選區(qū)域，使用基于SAT的形式化方法進(jìn)一步判斷。針對(duì)ISCAS′85基準(zhǔn)電路的實(shí)驗(yàn)結(jié)果表明，該方法具有較高的錯(cuò)誤診斷準(zhǔn)確性和效率。

參考文獻(xiàn)

[1]Veneris A G，Venkatraman S.Multiple Design Error Diagnosis and Correction in Digital VLSI Circuits.Proceedings of IEEE VLSI Test Symposium[C].1999:58-63.

[2]Jain A，Boppana V.Testing，Verification，and Diagnosis in the Presence of Unknowns.Proceedings of VLSI Test Symposium[C].2000:263-269.

[3]韓俊剛，杜慧敏.數(shù)字硬件的形式化驗(yàn)證[M].北京:北京大學(xué)出版社，2001.

[4]Shi-Yu Huang，Kwang-Ting Cheng.Error Tracer:Design Error Diagnosis Based on Fault Simulation Techniques[J].IEEE Trans.on Computer-Aided Design，1999，18 (9):1 341-1 352.

[5]Veneris A.Fault Diagnosis and Logic Debugging Using Boolean Satisfiability.Proceedings of International Workshop on Microprocessor Test and Verification Co-mmon Challenges and Solutions[C].2003:60-65.

[6]Boppana V，F(xiàn)ujita M.Modeling the Unknown! Towards Model-Independent Fault and Error Diagnosis.Proceedings of International Test Conference[C].1998:1 094-1 101.

[7]Boppana V，Mukherjee R，Jain J，et al.Multiple Error Diagnosis Based on Xlists.Proceedings of Design Automation Conference[C].1999:100-110.

[8]Aarna M，Raik J，Ubar R.Parallel Fault Simulation of Digi-tal Circuits .http:// main.rsf.rtu.lv/Latvieshu%201apa/ pasn_str/ konf/p_20.pdf.

[9]Tracy Larrabee.Test Pattern Generation using Boolean Sa-tisfiability [J].IEEE Trans.on Computer-aided Design of Integrated Circuits and Systems，1992，11 (1):4-15.

[10]Brand D.Verification of Large Synthesized Designs.Proceedings of International Conference of Computer-aided Design[C].1993:534-537.

Moskewicz M，Madigan C，Zhao Y，et al.Engineering an Efficient SAT Solver.Proceedings of Design Automation Conference[C].2001:530-535.