0 引 言
    錯(cuò)誤診斷是集成電路驗(yàn)證后期一個(gè)非常重要的階段，它幫助設(shè)計(jì)者在一個(gè)錯(cuò)誤芯片中預(yù)測(cè)錯(cuò)誤點(diǎn)，因此可以減輕整個(gè)調(diào)試過(guò)程中的工作量。經(jīng)過(guò)許多年的研究工作，組合電路的錯(cuò)誤診斷正趨于成熟和實(shí)用化。這些方法主要分為兩類(lèi)：基于模擬的方法和符號(hào)方法?；谀M的方法在每個(gè)錯(cuò)誤向量對(duì)電路的模擬中，通過(guò)過(guò)濾掉非錯(cuò)誤點(diǎn)而使含有錯(cuò)誤點(diǎn)的區(qū)域逐漸被限定下來(lái)。符號(hào)方法不用明確列舉錯(cuò)誤向量，而是主要依賴(lài)于二叉決策圖BDD，并提出錯(cuò)誤源定位的充分必要條件。依據(jù)此充分必要條件，可直接定位錯(cuò)誤點(diǎn)。該方法由于使用BDD技術(shù)，因而存在內(nèi)存爆炸的隱患。
    Boppana為錯(cuò)誤診斷提出了一個(gè)概括的基于區(qū)域的模型，該模型可以被擴(kuò)展來(lái)定位多錯(cuò)誤，并且可以用于解決時(shí)序電路的錯(cuò)誤診斷。Shi-Yu Huang提出了利用符號(hào)模擬來(lái)優(yōu)化拜占庭式錯(cuò)誤診斷的過(guò)程。Boppana介紹了一個(gè)基于Xlists模擬的診斷算法。N．Sridhar提出一種診斷技術(shù)，它通過(guò)可區(qū)分的X來(lái)消減錯(cuò)誤候選者區(qū)域。李光輝介紹了基于驗(yàn)證技術(shù)的錯(cuò)誤診斷方法，該方法將三值模擬與SAT技術(shù)相結(jié)合，以消減錯(cuò)誤空間，提高診斷結(jié)果。
    在此，提出一種利用符號(hào)模擬技術(shù)來(lái)優(yōu)化基于區(qū)域模型錯(cuò)誤診斷過(guò)程的方法。該方法首先使用基于區(qū)域模型錯(cuò)誤診斷方法中電路劃分方法對(duì)所要診斷的電路進(jìn)行區(qū)域劃分，然后在其基礎(chǔ)上利用符號(hào)模擬技術(shù)并使用兩個(gè)測(cè)量標(biāo)準(zhǔn)對(duì)各個(gè)區(qū)域的可疑度進(jìn)行等級(jí)排序?？梢啥仍礁叩膮^(qū)域包含錯(cuò)誤點(diǎn)的可能性越大。由于使用符號(hào)模擬技術(shù)，不需要對(duì)向量空間進(jìn)行明確列舉，因而所提出的方法在時(shí)間上是有效的。

1 定 義
    在此，將規(guī)范和實(shí)現(xiàn)分別表示為C1和C2，其中實(shí)現(xiàn)表示為一個(gè)組合的門(mén)級(jí)電路。規(guī)范和實(shí)現(xiàn)的主要輸入(PI)信號(hào)都表示為{x1，x2，…，xm)，其中m表示主要輸入的個(gè)數(shù)。規(guī)范和實(shí)現(xiàn)的主要輸出(PO)信號(hào)分別表示為{S1，S2，…，Sn}和{I1，I2，…In}，其中n表示主要輸出的個(gè)數(shù)。另外，假設(shè)預(yù)先生成的測(cè)試向量集合為T(mén)={v1，v2，…，vt}。
    定義1 (Si，Ii)被稱(chēng)為一個(gè)輸出對(duì)，其中1≤i≤n。 
    定義2 如果存在一個(gè)輸入測(cè)試向量v，使得v對(duì)規(guī)范和實(shí)現(xiàn)電路分別進(jìn)行模擬時(shí)，實(shí)現(xiàn)電路的輸出Ii與規(guī)范中相對(duì)應(yīng)的輸出Si的值不同，稱(chēng)Ii為錯(cuò)誤輸出或不匹配輸出，(Si，Ii)為不匹配輸出對(duì)。
    定義3 如果一個(gè)輸入向量能使任何輸出對(duì)之間產(chǎn)生不匹配現(xiàn)象，則稱(chēng)該輸入向量為錯(cuò)誤輸入向量。
    定義4 對(duì)一個(gè)不匹配輸出Ii的處理涉及到這樣一個(gè)機(jī)制，即對(duì)實(shí)現(xiàn)中某些信號(hào)注入二進(jìn)制值可以使Ii的響應(yīng)同規(guī)范中與它相對(duì)應(yīng)的輸出響應(yīng)相同。
    錯(cuò)誤診斷是基于一個(gè)被稱(chēng)為可治愈性的概念進(jìn)行的。在搜索錯(cuò)誤候選者的過(guò)程中，為了對(duì)每個(gè)信號(hào)的可疑度進(jìn)行等級(jí)排序，需要對(duì)每個(gè)信號(hào)進(jìn)行兩方面的測(cè)量：可治療的輸出數(shù)和可治療的向量數(shù)。
    定義5 假設(shè)實(shí)現(xiàn)電路在錯(cuò)誤輸入向量v，的模擬下，第i個(gè)主要輸出是不匹配輸出。令A(yù)是一個(gè)有著k個(gè)輸出{a1，a2，…，ak}的區(qū)域。如果在主要輸出Ii處的不匹配可以通過(guò)在{a1，a2，…ak}的一個(gè)注入組合來(lái)修正，則稱(chēng)Ii足在v的模擬下區(qū)域A的一個(gè)可治療輸出，用符號(hào)表示為Ii∈region_curable_output(A，v)。
    該定義說(shuō)明了可以通過(guò)對(duì)一個(gè)區(qū)域輸出進(jìn)行處理來(lái)糾正C2中出現(xiàn)的不匹配輸出。這里處理的方法是在區(qū)域輸出點(diǎn)注入某些二進(jìn)制值。由經(jīng)驗(yàn)可知，一個(gè)區(qū)域的可治療輸出的個(gè)數(shù)越多，則它成為包含錯(cuò)誤點(diǎn)區(qū)域的可能性越大，因?yàn)閷?duì)這個(gè)區(qū)域輸出值的改變會(huì)影響到較多的不匹配輸出。另外，除了這個(gè)測(cè)量標(biāo)準(zhǔn)，可以利用一個(gè)被稱(chēng)為可治療向量的測(cè)量標(biāo)準(zhǔn)來(lái)進(jìn)一步有效地檢查錯(cuò)誤點(diǎn)。
    定義6 如果實(shí)現(xiàn)電路C2在一個(gè)錯(cuò)誤輸入向量v的模擬下所產(chǎn)生的每個(gè)不匹配輸出可以同時(shí)通過(guò)在區(qū)域A的輸出{a1，a2，…，ak}處一個(gè)注入組合來(lái)糾正，并且不會(huì)產(chǎn)生新的不匹配輸出的話(huà)，則稱(chēng)這個(gè)錯(cuò)誤輸入向量v為區(qū)域A的可治療向量，用符號(hào)表示為Ii∈region_curable_vector(A)。如果這樣一個(gè)注入存在，則稱(chēng)它為區(qū)域A的一個(gè)可治療注入。
    基于這兩個(gè)測(cè)量標(biāo)準(zhǔn)，結(jié)合排序準(zhǔn)則，對(duì)每個(gè)區(qū)域的可疑度進(jìn)行等級(jí)排序。排序準(zhǔn)則如下：有較多可治療向量的區(qū)域，其成為錯(cuò)誤候選者的可疑度就越大。對(duì)于有相同數(shù)目可治療向量的區(qū)域，考慮它們的可治療輸出數(shù)目，即把可治療向量作為第一層測(cè)量標(biāo)準(zhǔn)使用，把可治療輸出作為第二層測(cè)量標(biāo)準(zhǔn)考慮。

2 區(qū)域模型介紹
    定義7電路中的任一門(mén)元件g與它的直接扇入門(mén)或者直接扇出門(mén)之間的距離稱(chēng)為一個(gè)結(jié)構(gòu)距離。
    定義8 給定d為一個(gè)固定化的結(jié)構(gòu)距離，g為電路的任一門(mén)元件，則以g為中心，以d為半徑的區(qū)域是集合D(g)={h|dis(g，h)≤d}。
    例如，門(mén)g周?chē)霃綖?的區(qū)域集合中包括g，g的直接扇出以及它的直接扇入。電路中的每個(gè)門(mén)都可以形成一個(gè)區(qū)域，因此電路中有多少個(gè)門(mén)就有多少個(gè)重疊區(qū)域。文獻(xiàn)[3]中介紹的基于區(qū)域模型的診斷方法是在模擬過(guò)程中，首先將區(qū)域中所有輸出結(jié)點(diǎn)設(shè)置為未知值X，以掩蓋發(fā)生在該區(qū)域中的任何錯(cuò)誤。如果對(duì)于一個(gè)給定向量v，沒(méi)有X可以傳播到一個(gè)主要輸出，則可以判定向量v探測(cè)不出區(qū)域中的任何錯(cuò)誤；否則說(shuō)明區(qū)域中存在錯(cuò)誤并將該區(qū)域作為一個(gè)錯(cuò)誤候選者。

3 符號(hào)模擬優(yōu)化過(guò)程
    接下來(lái)介紹如何將符號(hào)模擬技術(shù)應(yīng)用到區(qū)域模型上，并計(jì)算在錯(cuò)誤輸入向量v同時(shí)，對(duì)規(guī)范和實(shí)現(xiàn)電路進(jìn)行模擬的情況下，v是否為區(qū)域A的一個(gè)可治療向量。另外，需要確定在v的模擬下該區(qū)域有多少個(gè)可治療輸出。計(jì)算分四個(gè)主要步驟：無(wú)錯(cuò)誤邏輯模擬、符號(hào)注入、符號(hào)傳播及可治療性檢查。
   無(wú)錯(cuò)誤邏輯模擬簡(jiǎn)單確立了在輸入向量v的模擬下，每個(gè)信號(hào)線(xiàn)的無(wú)錯(cuò)誤邏輯值。下面要討論的其他3個(gè)步驟是針對(duì)區(qū)域模型等級(jí)排序提出的。
3．1 符號(hào)注入
    首先，將要考慮區(qū)域的輸出與區(qū)域之間的連接斷開(kāi)，接著把這些輸出信號(hào)線(xiàn)抽出來(lái)，將其中每一個(gè)信號(hào)線(xiàn)都視為一個(gè)偽主要輸入，最后對(duì)每個(gè)輸出端aj注入一個(gè)符號(hào)變量xj，其中1≤j≤k，k是區(qū)域A的輸出數(shù)量。注意：A輸出的扇出區(qū)域中每個(gè)信號(hào)都會(huì)受到注入變量的影響。圖1給出了注入符號(hào)前及注入符號(hào)后電路的基本情況。

3．2 符號(hào)傳播
    符號(hào)注入的作用是通過(guò)函數(shù)向主要輸出方向傳播來(lái)對(duì)區(qū)域A輸出的扇出區(qū)域中的信號(hào)進(jìn)行賦值。符號(hào)傳播的過(guò)程類(lèi)似于錯(cuò)誤模擬過(guò)程，不同之處在于符號(hào)傳播中一個(gè)信號(hào)的值不再是邏輯值0／1，而是用所注入的布爾變量{x1，x2，…，xk}表示的一個(gè)布爾函數(shù)。圖2所示為符號(hào)傳播過(guò)程。
    在符號(hào)傳播過(guò)程中可以采取兩項(xiàng)技術(shù)來(lái)加速該過(guò)程。一個(gè)是有序二叉決策圖(OBDD)的使用，另一個(gè)是事件驅(qū)動(dòng)的模擬。BDD的使用有可能造成內(nèi)存爆炸，但是這里由于診斷過(guò)程中不需要特征化電路的全局函數(shù)，因此避免了上述內(nèi)存爆炸問(wèn)題。在事件驅(qū)動(dòng)模擬中，許多門(mén)元件由于不受符號(hào)注入的影響，不需要進(jìn)行再次模擬，因此在符號(hào)傳播的一次單一運(yùn)行中，CPU的處理時(shí)間不會(huì)因?yàn)殡娐芬?guī)模的增大而迅速增加。
3．3 可治療性檢查
    符號(hào)傳播過(guò)程的最后可以在實(shí)現(xiàn)電路的每個(gè)主要輸出得到一個(gè)布爾函數(shù)，稱(chēng)為作用函數(shù)。一個(gè)作用函數(shù)包含它對(duì)區(qū)域輸出{a1，a2，…，ak}的一個(gè)注入起怎樣反應(yīng)的相關(guān)信息。通過(guò)對(duì)這些信息的獲得可以計(jì)算區(qū)域中可治療輸入和可治療輸出的個(gè)數(shù)。
    定義9 令I(lǐng)i是第i個(gè)主要輸出。v是一個(gè)錯(cuò)誤輸入向量，A是一個(gè)待檢查的錯(cuò)誤候選者區(qū)域。在向量v對(duì)實(shí)現(xiàn)電路進(jìn)行模擬以及對(duì)區(qū)域A的輸出進(jìn)行符號(hào)注入和符號(hào)傳播過(guò)程后，Ii的作用函數(shù)表示為Reacti(v，a，X)，其中X是執(zhí)行符號(hào)注入時(shí)所使用的布爾變量{x1，x2，…，xk}的集合。
    命題1 當(dāng)且僅當(dāng)下面式子成立時(shí)，錯(cuò)誤輸入向量v是區(qū)域A的一個(gè)可治療向量。Si(v)表示在向量v模擬下規(guī)范的第i個(gè)輸出響應(yīng)，n是輸出的總個(gè)數(shù)。

   
    證明 如果存在{x1，x2，…，xk}的一個(gè)注入組合，使得注入后對(duì)于每一個(gè)主要輸出索引i，實(shí)現(xiàn)電路的Reacti(v，a，X)的響應(yīng)同規(guī)范Si(v)的響應(yīng)值相同，則該注入組合被稱(chēng)為區(qū)域可治療注入，同時(shí)也證明了在區(qū)域A的輸出處注入的組合使得錯(cuò)誤輸入向量v不再引起任何輸出對(duì)之間的不匹配現(xiàn)象，即v不再是實(shí)現(xiàn)電路的一個(gè)錯(cuò)誤輸入向量。
    如果存在一個(gè)注入組合，使得一個(gè)不匹配輸出的邏輯值變?yōu)榕c它對(duì)應(yīng)的完全相同的值，則稱(chēng)該不匹配輸出為一個(gè)區(qū)域可治療輸出(區(qū)域可治療輸出的規(guī)則)：如果下面的條件成立，則對(duì)于向量v，一個(gè)不匹配輸出Zic稱(chēng)為通過(guò)區(qū)域輸出信號(hào)a的可治療輸出。

   
    例如(區(qū)域可治療注入)考慮圖中的規(guī)范和實(shí)現(xiàn)，在一個(gè)輸入向量v的模擬下，規(guī)范的輸出響應(yīng)為(0，O，0，0，0)，而實(shí)現(xiàn)的響應(yīng)為(0，0，0，1，1)。第四和第五個(gè)輸出為不匹配輸出。通過(guò)執(zhí)行符號(hào)注入和傳播，每個(gè)主要輸出作用函數(shù)的集合為{0，0，x3，x1，(x1x2)'}。
    前兩個(gè)輸出對(duì)是匹配的，因此只進(jìn)行后三個(gè)輸出的可治療性檢查。為了檢查可治療向量，注入需滿(mǎn)足(x3三0)，(x1三O)和[(x1x2)'三0]。因?yàn)榈诙€(gè)和第三個(gè)條件互相沖突，可得出結(jié)論：區(qū)域A不能通過(guò)注入來(lái)治療錯(cuò)誤輸入向量v。

    另一方面，為可治療輸出檢查每個(gè)作用函數(shù)。在注入前只需要關(guān)注于第4和第5個(gè)不匹配輸出。第4個(gè)輸出的作用函數(shù)是x1，只需要在注入時(shí)使x1為0，就可使輸出從1變?yōu)?，即通過(guò)此方法解決了第4個(gè)輸出的不匹配問(wèn)題，因此第4個(gè)輸出是一個(gè)可治療輸出。類(lèi)似地，第5個(gè)輸出也是可治療輸出。因此該區(qū)域A共有兩個(gè)可治療輸出。在這個(gè)例子中，兩個(gè)不匹配輸出可以分別獨(dú)立地進(jìn)行治療糾正；然而在治療最后一個(gè)輸出時(shí)將不可避免地在第3個(gè)輸出點(diǎn)引出一個(gè)新的不匹配問(wèn)題，這也是給定的錯(cuò)誤輸入向量不能通過(guò)區(qū)域A來(lái)治療糾正的原因。利用符號(hào)模擬技術(shù)可以?xún)?yōu)化基于區(qū)域模型進(jìn)行錯(cuò)誤診斷的過(guò)程，依據(jù)區(qū)域可治療向量和區(qū)域可治療輸出兩個(gè)測(cè)量標(biāo)準(zhǔn)對(duì)候選的各個(gè)區(qū)域進(jìn)行包含錯(cuò)誤點(diǎn)的可疑度等級(jí)排序，可疑度等級(jí)越高的區(qū)域，包含錯(cuò)誤點(diǎn)的可能性也越大。

4 實(shí)驗(yàn)結(jié)果與結(jié)論
    在此選取幾個(gè)簡(jiǎn)單的組合電路，每個(gè)電路隨機(jī)注入一個(gè)門(mén)置換錯(cuò)誤，利用符號(hào)模擬技術(shù)對(duì)每個(gè)電路進(jìn)行錯(cuò)誤診斷。從方法執(zhí)行的CPU時(shí)間來(lái)看，這里提出的優(yōu)化方法并不是每次都比原始基于區(qū)域模型的方法運(yùn)行速度快，但是從整體來(lái)看，因?yàn)樵搩?yōu)化方法極大地減少了所要處理候選區(qū)域的個(gè)數(shù)，因此總運(yùn)行時(shí)間還是比較理想的。
    這里提出將符號(hào)模擬技術(shù)應(yīng)用到基于區(qū)域模型的錯(cuò)誤診斷方法中的新方法。該方法采用符號(hào)模擬技術(shù)對(duì)候選區(qū)域進(jìn)行處理，包括符號(hào)的注入，符號(hào)的傳播，可治療性檢查三步。另外，用符號(hào)模擬的方法對(duì)區(qū)域進(jìn)行處理后得到的部分處理信息可以應(yīng)用到后面的糾錯(cuò)過(guò)程中，這點(diǎn)是原始基于區(qū)域模型方法中所不具有的。利用符號(hào)模擬的錯(cuò)誤診斷方法也可以擴(kuò)展應(yīng)用到具有多錯(cuò)誤的電路中，但是尚需進(jìn)一步研究與實(shí)現(xiàn)。