摘要:引入布爾差分的思想,對被測電路函數的BDD結構進行判斷生成測試向量。本方案較傳統的以圖進行搜索的ATPG方法有效地減少了時空開銷,并將布爾差分的理論方法應用于實際。實驗表明,本方案可以有效地進行測試生成。
關鍵詞:二元決策圖; 布爾差分; 自動測試向量生成
中圖分類號:TP331文獻標志碼:A
文章編號:1001-3695(2008)05-1450-03
在數字系統的測試中,ATPG是對測試電路產生測試向量的過程[1]。通常ATPG算法首先給電路插入一個故障;然后通過在電路輸入端激活這個故障,并將其產生的響應通過電路傳播到輸出端。若輸出信號與無故障電路的期望值不同,就可以檢測到這個故障了。針對組合電路中固定型故障,目前存在一些ATPG算法。最基本的是布爾差分法[2,3]。它描述嚴格,是研究組合電路測試生成的理論基礎。最經典的是Roth的D算法[4],采用D立方建立了ATPG的運算。此外還有Geol的PODEM算法、Fujiwara的FAN算法[6]等,在回溯和加快搜索速度上作出了很大的貢獻。Geol在其PODEM算法[5]中采用二元決策樹(binary decision tree,BDT)進行搜索。Akers[7]提出的使用BDD來表述邏輯電路則更為實際。近年來,BDD的理論有了更進一步的完善和發展[8,9],并更多地運用到數字電路設計中的驗證、綜合[10]及自動測試模式生成[11]。
本文嘗試采用簡潔的簡化排序二元決策圖(reduced ordered BDD,ROBDD)來對組合電路進行表示及運算;同時融入布爾差分的思想,對被測電路BDD結構進行判斷,從而進行測試生成。
1BDD的相關知識
1.1使用BDD表示布爾函數
對式(1),將x1分別設置為0值和1值時,在運算中就會產生兩種不同的情況,以圖的形式表述如圖1(a)(圖中的虛線邊表示節點變量取0值,為節點的左后繼;同理實線邊表示取1值,為右后繼)所示。接下來繼續對此函數中的另外兩個變量x2和x3也進行同樣的展開操作,直至全部變量都被展開。至此,布爾函數f=(x1∧x2)x3中可能的變量取值及運算結果全部由圖1(b)表示。
圖1(b)稱為二元決策樹。Geol首先在組合電路ATPG的文獻[5]中采用這種二元樹。一個表示含有n個變量函數的二元決策樹中有2(n+1)-1個節點,這對于含有變量較多的布爾函數表述的開銷是很大的。
注意到在對函數生成決策樹時根據一定的變量順序(圖1(b)中的(x1,x2,x3)),并且處于樹的同一層的節點標記一樣(圖1(b)中自上向下第二層均為x2),這種決策樹稱做排序二元決策樹。在決策樹的形式中,存在很多重復的相同節點(特別是終節點,圖1(b))。通過相應的化簡,可以得到排序決策樹相對應的BDD形式。在此引入節點冗余和節點等價的概念。
定義1對于一個決策樹(或決策圖)中的任一節點,如果其左右后繼相同,則此節點為冗余節點。
定義2對于一個決策樹(或決策圖)中的任意兩個節點,如果它們具有相同的標記、左后繼及右后繼,則這兩個節點稱為等價節點。
如圖1(b)中自上而下第二層中左邊的x2節點為冗余節點,第三層中自左向右第1、2、3個x3節點均兩兩為等價節點。針對上述兩種情況的節點,可以采取相應的化簡操作進行化簡。節點化簡操作如下:
a)如果節點a為冗余節點,則將節點a刪除并將其所有入邊指向其任一后繼;
b)如果節點a和b等價,則刪除節點b并將其所有入邊指向節點a。
通過以上兩個操作對圖1(b)進行相應的化簡,繼而生成函數f=(x1∧x2)x3所對應的BDD(圖2)。BDD是一個有根節點的有向無環圖(DAG),含有一個或兩個出度為0的終節點(即0或1節點)、若干出度為2的內部節點。對于一個含有n個變量的函數,其對應BDD的節點個數范圍為[n+2,2n+1](上限為理論值,實際中很難達到),相對于BDT的表達方式,時間空間開銷大量減少,對于表述函數更為實際有效。
對于函數F,將其變量根據一定的順序(x1,x2,x3,…,xn)生成的BDD稱為OBDD (ordered BDD,排序二元決策圖)。當OBDD滿足非冗余性(不存在冗余節點)及惟一性(不存在等價節點)時,被稱為ROBDD (reduced OBDD,簡化排序二元決策圖),簡稱BDD。
1.2BDD間的同構
筆者注意到定義2中提到的兩個節點等價的情況是發生在同一個圖中,將這種情況擴展到兩個圖之間,就得到了同構的定義。
定義3兩個決策圖D和H,如果從圖G的節點到圖H的節點存在一個一對一的映射關系σ:vD→vH。當vD和vH是終節點時它們的值相等;當vD和vH是內部節點時它們的標記、左后繼及右后繼相等,那么稱圖D和圖H是同構的。
根據定義3,對于同一個BDD中的兩個等價節點,如果把它們及其各自的左右后繼形成的圖看做子圖,那么這兩個子圖間是同構的。
1.3BDD的構造及運算
BDD構造算法中i表示當前處理的變量序號,即當前對變量xi進行香農展開;t為當前要展開的式子;t[xi=0]表示對式子t中的xi賦值0值后得到的式子。該構造過程執行時,通過遞歸的方式由終節點向根節點生成決策圖。節點是BDD中的基本元素。對于圖中的每一個節點vi(對應標記序號為i的變量),用一個三元組Node(i, l, h)來記錄。其中:i表示相應的變量序號;l和h分別為該節點的左后繼和右后繼。生成節點的過程NodeGen(i, l, h)處在構造過程的最后一步,其作用是對在BDD生成過程中所產生的節點,經查找如果存在于已生成的節點列表中則直接調用;否則生成新節點并保存,從而避免了冗余和等價節點的出現。
兩個BDD圖D與H間的運算,就是圖D與H中節點間的運算。對于分屬于兩個BDD的當前正在運算的兩個節點vD和vH,節點u為它們運算得到的結果節點:a)若均為終節點,則直接運算產生節點u;b)若所對應變量序號相同,則此序號為節點u的序號,v1和v2的左后繼的運算結果為u的左后繼,同理得到u的右后繼;c)若所對應變量序號不同,則較小序號為節點u的序號,序號較小節點的左后繼與序號較大節點的運算結果為u的左后繼,同理得到u的右后繼。終節點0或1對應的var值為varmax+1。算法2中的表G用來記錄已生成的節點,以防止產生冗余及等價節點。BDD運算過程從根節點開始通過遞歸調用app對兩個圖之間進行計算,生成新的BDD的各個節點。
2基于BDD的測試生成
在組合電路的測試生成算法中,布爾差分是一種理論嚴格的測試生成方法。
4結束語
本文提出一種新的組合電路測試生成方法。本方法使用簡潔高效的ROBDD作為電路表述和運算的載體,較傳統圖的方法有著更低的時間空間開銷。同時本方法嘗試將布爾差分這種完善的理論分析方法的思想結合圖的特點引入實際應用。經實驗證明,本方法針對被測電路中特定的固定型故障,可以有效地生成該故障的全部測試向量,這同時也為測試集壓縮提供了基礎。
參考文獻:
[1]BUSHNELL M D, AGRAWAL V D. 超大規模集成電路測試——數字、存儲器和混合信號系統[M].蔣安平,等譯.北京:電子工業出版社,2005.
[2]閔應驊.邏輯電路測試[M].北京:中國鐵道出版社,1986.
[3]楊士元.數字系統的故障診斷與可靠性設計[M].北京:清華大學出版社,2000.
[4]ROTH J P.Diagnosis of automata failures: a calculus and a method[J].IBM Journal of Research and Development, 1996,10(4):278-291.
[5]GOEL P.An implicit enumeration algorithm to generate tests for combinational logic circuits[J].IEEE Trans on Computers,1981,30(3):215-222.
[6]FUJIWARA H.FAN: a fanout-oriented test pattern generation algorithm[C]//Proc of International Symp on Circuits and Systems. 1985:671-674.
[7]AKERS S B.Binary decision diagrams[J].IEEE Trans on Compu-ters, 1978,27(6):66-73.
[8]BRYANT R E.Graph-based algorithms for Boolean function manipulation[J].IEEE Trans on Computers,1986,35(8):677-691.
[9]CHEN Y A,BRYANT R E.An efficient graph representation for arithmetic circuit verification[J].IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems, 2001,20(12):1442-1454.
[10]李光輝,邵明,李曉維.基于BDD的組合電路等價性檢驗方法[J].微電子學與計算機,2003,20(2):48-51.
[11]ABADIR M S,REGHBATI H K.Functional test generation for digital circuits described using binary decision diagrams computers[J].IEEE Trans on Computers,1986,35(4):375-379.
[12]SOMENZI F.CUDD: CU decision diagram package release 2.3.1[EB/OL].(2001).http://vlsi.colorado.edu/~fabio/CUDD/.
“本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文”