|
1 引 言 錯誤診斷是集成電路驗證后期一個非常重要的階段，它幫助設計者在一個錯誤芯片中預測錯誤點，因此可以減輕整個調(diào)試過程中的工作量。經(jīng)過許多年的研究工作，組合電路的錯誤診斷正趨于成熟和實用化。這些方法主要分為兩類：基于模擬的方法和符號方法。基于模擬的方法在每個錯誤向量對電路的模擬中，通過過濾掉非錯誤點而使含有錯誤點的區(qū)域逐漸被限定下來。符號方法不用明確列舉錯誤向量，而是主要依賴于二叉決策圖BDD，并提出錯誤源定位的充分必要條件。依據(jù)此充分必要條件，可直接定位錯誤點。該方法由于使用BDD技術，因而存在內(nèi)存爆炸的隱患。 Boppana為錯誤診斷提出了一個概括的基于區(qū)域的模型，該模型可以被擴展來定位多錯誤，并且可以用于解決時序電路的錯誤診斷。Shi-Yu Huang提出了利用符號模擬來優(yōu)化拜占庭式錯誤診斷的過程。Boppana介紹了一個基于Xlists模擬的診斷算法。N．Sridhar提出一種診斷技術，它通過可區(qū)分的X來消減錯誤候選者區(qū)域。李光輝介紹了基于驗證技術的錯誤診斷方法，該方法將三值模擬與SAT技術相結合，以消減錯誤空間，提高診斷結果。 在此，提出一種利用符號模擬技術來優(yōu)化基于區(qū)域模型錯誤診斷過程的方法。該方法首先使用基于區(qū)域模型錯誤診斷方法中電路劃分方法對所要診斷的電路進行區(qū)域劃分，然后在其基礎上利用符號模擬技術并使用兩個測量標準對各個區(qū)域的可疑度進行等級排序。可疑度越高的區(qū)域包含錯誤點的可能性越大。由于使用符號模擬技術，不需要對向量空間進行明確列舉，因而所提出的方法在時間上是有效的。 2 定 義 在此，將規(guī)范和實現(xiàn)分別表示為C1和C2，其中實現(xiàn)表示為一個組合的門級電路。規(guī)范和實現(xiàn)的主要輸入(PI)信號都表示為{x1，x2，…，xm)，其中 m表示主要輸入的個數(shù)。規(guī)范和實現(xiàn)的主要輸出(PO)信號分別表示為{S1，S2，…，Sn}和{I1，I2，…In}，其中n表示主要輸出的個數(shù)。另外，假設預先生成的測試向量集合為T={v1，v2，…，vt}。 定義1 (Si，Ii)被稱為一個輸出對，其中1≤i≤n。 定義2 如果存在一個輸入測試向量v，使得v對規(guī)范和實現(xiàn)電路分別進行模擬時，實現(xiàn)電路的輸出Ii與規(guī)范中相對應的輸出Si的值不同，稱Ii為錯誤輸出或不匹配輸出，(Si，Ii)為不匹配輸出對。 定義3 如果一個輸入向量能使任何輸出對之間產(chǎn)生不匹配現(xiàn)象，則稱該輸入向量為錯誤輸入向量。 定義4 對一個不匹配輸出Ii的處理涉及到這樣一個機制，即對實現(xiàn)中某些信號注入二進制值可以使Ii的響應同規(guī)范中與它相對應的輸出響應相同。 錯誤診斷是基于一個被稱為可治愈性的概念進行的。在搜索錯誤候選者的過程中，為了對每個信號的可疑度進行等級排序，需要對每個信號進行兩方面的測量：可治療的輸出數(shù)和可治療的向量數(shù)。 定義5 假設實現(xiàn)電路在錯誤輸入向量v，的模擬下，第i個主要輸出是不匹配輸出。令A是一個有著k個輸出{a1，a2，…，ak}的區(qū)域。如果在主要輸出Ii處的不匹配可以通過在{a1，a2，…ak}的一個注入組合來修正，則稱Ii足在v的模擬下區(qū)域A的一個可治療輸出，用符號表示為 Ii∈region_curable_output(A，v)。 該定義說明了可以通過對一個區(qū)域輸出進行處理來糾正C2中出現(xiàn)的不匹配輸出。這里處理的方法是在區(qū)域輸出點注入某些二進制值。由經(jīng)驗可知，一個區(qū)域的可治療輸出的個數(shù)越多，則它成為包含錯誤點區(qū)域的可能性越大，因為對這個區(qū)域輸出值的改變會影響到較多的不匹配輸出。另外，除了這個測量標準，可以利用一個被稱為可治療向量的測量標準來進一步有效地檢查錯誤點。 定義6 如果實現(xiàn)電路C2在一個錯誤輸入向量v的模擬下所產(chǎn)生的每個不匹配輸出可以同時通過在區(qū)域A的輸出{a1，a2，…，ak}處一個注入組合來糾正，并且不會產(chǎn)生新的不匹配輸出的話，則稱這個錯誤輸入向量v為區(qū)域A的可治療向量，用符號表示為Ii∈region_curable_vector(A)。如果這樣一個注入存在，則稱它為區(qū)域A的一個可治療注入。 基于這兩個測量標準，結合排序準則，對每個區(qū)域的可疑度進行等級排序。排序準則如下：有較多可治療向量的區(qū)域，其成為錯誤候選者的可疑度就越大。對于有相同數(shù)目可治療向量的區(qū)域，考慮它們的可治療輸出數(shù)目，即把可治療向量作為第一層測量標準使用，把可治療輸出作為第二層測量標準考慮。 3 區(qū)域模型介紹 定義7電路中的任一門元件g與它的直接扇入門或者直接扇出門之間的距離稱為一個結構距離。 定義8 給定d為一個固定化的結構距離，g為電路的任一門元件，則以g為中心，以d為半徑的區(qū)域是集合D(g)={h|dis(g，h)≤d}。 例如，門g周圍半徑為1的區(qū)域集合中包括g，g的直接扇出以及它的直接扇入。電路中的每個門都可以形成一個區(qū)域，因此電路中有多少個門就有多少個重疊區(qū)域。文獻中介紹的基于區(qū)域模型的診斷方法是在模擬過程中，首先將區(qū)域中所有輸出結點設置為未知值X，以掩蓋發(fā)生在該區(qū)域中的任何錯誤。如果對于一個給定向量v，沒有X可以傳播到一個主要輸出，則可以判定向量v探測不出區(qū)域中的任何錯誤；否則說明區(qū)域中存在錯誤并將該區(qū)域作為一個錯誤候選者。 4 符號模擬優(yōu)化過程 接下來介紹如何將符號模擬技術應用到區(qū)域模型上，并計算在錯誤輸入向量v同時，對規(guī)范和實現(xiàn)電路進行模擬的情況下，v是否為區(qū)域A的一個可治療向量。另外，需要確定在v的模擬下該區(qū)域有多少個可治療輸出。計算分四個主要步驟：無錯誤邏輯模擬、符號注入、符號傳播及可治療性檢查。 無錯誤邏輯模擬簡單確立了在輸入向量v的模擬下，每個信號線的無錯誤邏輯值。下面要討論的其他3個步驟是針對區(qū)域模型等級排序提出的。 4．1 符號注入 首先，將要考慮區(qū)域的輸出與區(qū)域之間的連接斷開，接著把這些輸出信號線抽出來，將其中每一個信號線都視為一個偽主要輸入，最后對每個輸出端aj注入一個符號變量xj，其中1≤j≤k，k是區(qū)域A的輸出數(shù)量。注意：A輸出的扇出區(qū)域中每個信號都會受到注入變量的影響。圖1給出了注入符號前及注入符號后電路的基本情況。 4．2 符號傳播 符號注入的作用是通過函數(shù)向主要輸出方向傳播來對區(qū)域A輸出的扇出區(qū)域中的信號進行賦值。符號傳播的過程類似于錯誤模擬過程，不同之處在于符號傳播中一個信號的值不再是邏輯值0／1，而是用所注入的布爾變量{x1，x2，…，xk}表示的一個布爾函數(shù)。圖2所示為符號傳播過程。 在符號傳播過程中可以采取兩項技術來加速該過程。一個是有序二叉決策圖(OBDD)的使用，另一個是事件驅(qū)動的模擬。BDD的使用有可能造成內(nèi)存爆炸，但是這里由于診斷過程中不需要特征化電路的全局函數(shù)，因此避免了上述內(nèi)存爆炸問題。在事件驅(qū)動模擬中，許多門元件由于不受符號注入的影響，不需要進行再次模擬，因此在符號傳播的一次單一運行中，CPU的處理時間不會因為電路規(guī)模的增大而迅速增加。 4．3 可治療性檢查 符號傳播過程的最后可以在實現(xiàn)電路的每個主要輸出得到一個布爾函數(shù)，稱為作用函數(shù)。一個作用函數(shù)包含它對區(qū)域輸出{a1，a2，…，ak}的一個注入起怎樣反應的相關信息。通過對這些信息的獲得可以計算區(qū)域中可治療輸入和可治療輸出的個數(shù)。 定義9 令Ii是第i個主要輸出。v是一個錯誤輸入向量，A是一個待檢查的錯誤候選者區(qū)域。在向量v對實現(xiàn)電路進行模擬以及對區(qū)域A的輸出進行符號注入和符號傳播過程后，Ii的作用函數(shù)表示為Reacti(v，a，X)，其中X是執(zhí)行符號注入時所使用的布爾變量{x1，x2，…，xk}的集合。 命題1 當且僅當下面式子成立時，錯誤輸入向量v是區(qū)域A的一個可治療向量。Si(v)表示在向量v模擬下規(guī)范的第i個輸出響應，n是輸出的總個數(shù)。 證明如果存在{x1，x2，…，xk}的一個注入組合，使得注入后對于每一個主要輸出索引i，實現(xiàn)電路的Reacti(v，a，X)的響應同規(guī)范Si(v)的響應值相同，則該注入組合被稱為區(qū)域可治療注入，同時也證明了在區(qū)域A的輸出處注入的組合使得錯誤輸入向量v不再引起任何輸出對之間的不匹配現(xiàn)象，即v不再是實現(xiàn)電路的一個錯誤輸入向量。 如果存在一個注入組合，使得一個不匹配輸出的邏輯值變?yōu)榕c它對應的完全相同的值，則稱該不匹配輸出為一個區(qū)域可治療輸出(區(qū)域可治療輸出的規(guī)則)：如果下面的條件成立，則對于向量v，一個不匹配輸出Zic稱為通過區(qū)域輸出信號a的可治療輸出。 例如(區(qū)域可治療注入)考慮圖中的規(guī)范和實現(xiàn)，在一個輸入向量v的模擬下，規(guī)范的輸出響應為(0，O，0，0，0)，而實現(xiàn)的響應為 (0，0，0，1，1)。第四和第五個輸出為不匹配輸出。通過執(zhí)行符號注入和傳播，每個主要輸出作用函數(shù)的集合為{0，0，x3，x1， (x1x2)'}。 前兩個輸出對是匹配的，因此只進行后三個輸出的可治療性檢查。為了檢查可治療向量，注入需滿足(x3三0)，(x1三O)和[(x1x2)'三0]。因為第二個和第三個條件互相沖突，可得出結論：區(qū)域A不能通過注入來治療錯誤輸入向量v。 另一方面，為可治療輸出檢查每個作用函數(shù)。在注入前只需要關注于第4和第5個不匹配輸出。第4個輸出的作用函數(shù)是x1，只需要在注入時使x1為0，就可使輸出從1變?yōu)?，即通過此方法解決了第4個輸出的不匹配問題，因此第4個輸出是一個可治療輸出。類似地，第5個輸出也是可治療輸出。因此該區(qū)域A共有兩個可治療輸出。在這個例子中，兩個不匹配輸出可以分別獨立地進行治療糾正；然而在治療最后一個輸出時將不可避免地在第3個輸出點引出一個新的不匹配問題，這也是給定的錯誤輸入向量不能通過區(qū)域A來治療糾正的原因。利用符號模擬技術可以優(yōu)化基于區(qū)域模型進行錯誤診斷的過程，依據(jù)區(qū)域可治療向量和區(qū)域可治療輸出兩個測量標準對候選的各個區(qū)域進行包含錯誤點的可疑度等級排序，可疑度等級越高的區(qū)域，包含錯誤點的可能性也越大。 5 實驗結果與結論 在此選取幾個簡單的組合電路，每個電路隨機注入一個門置換錯誤，利用符號模擬技術對每個電路進行錯誤診斷。從方法執(zhí)行的CPU時間來看，這里提出的優(yōu)化方法并不是每次都比原始基于區(qū)域模型的方法運行速度快，但是從整體來看，因為該優(yōu)化方法極大地減少了所要處理候選區(qū)域的個數(shù)，因此總運行時間還是比較理想的。 這里提出將符號模擬技術應用到基于區(qū)域模型的錯誤診斷方法中的新方法。該方法采用符號模擬技術對候選區(qū)域進行處理，包括符號的注入，符號的傳播，可治療性檢查三步。另外，用符號模擬的方法對區(qū)域進行處理后得到的部分處理信息可以應用到后面的糾錯過程中，這點是原始基于區(qū)域模型方法中所不具有的。利用符號模擬的錯誤診斷方法也可以擴展應用到具有多錯誤的電路中，但是尚需進一步研究與實現(xiàn)。 |
