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

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

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

3．2 符號傳播
符號注入的作用是通過函數向主要輸出方向傳播來對區域A輸出的扇出區域中的信號進行賦值。符號傳播的過程類似于錯誤模擬過程，不同之處在于符號傳播中一個信號的值不再是邏輯值0／1，而是用所注入的布爾變量{x1，x2，…，xk}表示的一個布爾函數。圖2所示為符號傳播過程。