基于有界模型檢測的門級軟件自測試方法

張 穎， 張嘉琦， 王 真， 江建慧

(1. 同濟大學 軟件學院, 上海 201804； 2. 上海電力學院 計算機科學與技術學院, 上海 200090)

由于處理器主頻的不斷升級而外部測試儀的速度提升緩慢且造價昂貴，因此直接使用外部測試儀對處理器進行實速測試變得越來越困難.一方面，處理器的很多故障只有在實速條件下才能被激活；另一方面，用戶有強烈的處理器現(xiàn)場測試需求.因此，迫切需要一種在線測試方法能夠?qū)嵥贉y試處理器.

研究人員提出了針對處理器的多種實速測試方法，如內(nèi)建自測試(BIST)方法[1-2].然而，BIST方法導致大量性能和面積開銷，同時BIST電路的功耗較大,可能會損傷處理器電路.隨后研究人員提出了基于軟件的自測試(SBST)方法[3-4].通過運行正常程序測試處理器自身的結(jié)構(gòu)和功能故障，在不引入任何硬件開銷的前提下，完成處理器的在線測試.SBST方法是非侵入式測試方法，避免了過度測試，而且可以在現(xiàn)場條件下進行實速測試.然而，處理器的控制模塊是復雜的時序電路，現(xiàn)有的SBST方法難以直接采用測試向量自動生成(ATPG)技術產(chǎn)生時序電路的測試向量.控制模塊是處理器的關鍵模塊，研究新的指令級自測試方法來有效檢測測試控制模塊中的難測故障是非常必要的.

本文采用有界模型檢測(BMC)方法[5-6]，針對處理器的控制器中難測故障，在門級電路上直接產(chǎn)生測試程序.

1 相關工作介紹

1.1 基于軟件的自測試方法

SBST方法通過運行程序直接檢測處理器中功能與結(jié)構(gòu)故障.這種方法不需要引入任何硬件開銷，就能夠在線測試處理器，并且達到理想的故障覆蓋率，已經(jīng)成為一種非常理想的測試方法.

如圖1所示，SBST方法可以分為以下3步：① 下載測試程序與測試數(shù)據(jù)到片上系統(tǒng)；② 處理器執(zhí)行測試程序，將測試向量施加到被測模塊上，激活被測故障；③ 測試響應被保存在存儲器中，并上傳到外界用于觀察.

圖1 處理器的基于軟件的自測試方法示意圖[7]Fig.1 Framework of SBST method on processors[7]

近年來，SBST技術得到迅速發(fā)展，有學者使用測試指令自動生成(ATIG)方法自動產(chǎn)生SBST程序，取得了較好的效果[8-12].然而，處理器中的控制模塊結(jié)構(gòu)復雜，而且是時序電路,目前除了使用侵入式掃描鏈測試方法，其他方法均難以有效測試模塊故障.侵入式掃描鏈測試方法無法在線測試，需要大量額外的測試開銷，因此本文提出一種可以更加有效測試控制模塊的軟件自測試方法.

1.2 有界模型檢測

BMC[5-6]是一種很重要的自動驗證技術,它不僅可以自動驗證有窮狀態(tài)系統(tǒng)中命題的正確性，一旦命題有錯，它還能夠提供不滿足命題的違例.因此，采用BMC方法能夠在控制器的門級電路上，直接獲得觸發(fā)難測故障性質(zhì)的測試序列.由于BMC方法窮盡地搜索了所有測試序列，因此能夠控制故障難以觸發(fā)的問題，進而在控制器上達到良好的測試效果.

控制模塊受處理器中其他模塊的約束，僅在控制模塊上運行BMC，無法產(chǎn)生滿足現(xiàn)場測試要求的測試序列.然而，將整個處理器輸入到BMC工具中，由于處理器規(guī)模較大，會遭遇狀態(tài)爆炸問題.本文擬將處理器的其他模塊抽象成簡單的功能約束，緩解BMC的狀態(tài)爆炸問題.

1.3 測試指令自動生成方法

ATIG[9]是一種新型測試技術，它能夠自動生成處理器的自測試程序.通?；诩拇嫫鱾鬏敿?RTL)軟件的自測試方法需要人工生成測試程序，而ATIG方法首次實現(xiàn)了測試程序的自動生成.首先，通過數(shù)據(jù)挖掘獲得擴展指令和信號之間的映射，并將指令中數(shù)據(jù)的范圍映射到信號上，作為指令級約束;其次，將基于指令級的約束轉(zhuǎn)化為虛擬電路并連接到被測電路上，然后自動生成測試向量;最后，根據(jù)測試向量中控制信號的值和映射關系，將測試向量轉(zhuǎn)化為測試指令，形成測試程序.ATIG方法尚未提出針對處理器中時序控制單元的測試生成方法，這種控制模塊的故障覆蓋率仍有待提高.

2 基于BMC方法的門級軟件自測試方法

本文提出了基于BMC方法的門級軟件自測試(GB-SBST)方法.該方法能夠針對控制模塊中的難測故障產(chǎn)生測試程序，有效測試時序的控制模塊，進一步提升現(xiàn)有ATIG方法的測試效果.

具體而言，本文方法專門針對ATIG方法未檢測到的故障，采用BMC方法來獲取能觸發(fā)該故障的指令序列，最后通過觀測指令序列得到測試響應.圖2展示了本文方法的流程.對于所有未檢測的故障逐個產(chǎn)生測試程序，包括以下3個主要步驟：① 模型化被測電路，并采用抽象的方法進行簡化；② 將選中的故障轉(zhuǎn)化成性質(zhì)，運行BMC，搜索激活該性質(zhì)的違例；③ 若獲得違例，則將違例中輸入信號序列映射成測試指令序列，最后添加觀測指令序列，從而生成指令級自測試程序.

圖2 基于有界模型檢測的門級軟件自測試方法流程Fig.2 Flow chart of GB-SBST method

2.1 模型的獲得與簡化

目前使用的BMC工具NuSMV[13]只能處理采用smv語言[14]編寫的設計，被測電路的門級電路需要采用smv語言建模描述.由于門級電路中的組合門對應smv語言中的線變量，時序的寄存器對應smv語言中的狀態(tài)變量，因此編寫了一個轉(zhuǎn)化程序，將被測電路的門級電路文件直接轉(zhuǎn)化成smv語言描述的文件.

被測模塊在處理器內(nèi)部，它受到眾多其他模塊的影響，單獨的被測模塊無法模擬其在正常模式下的功能.然而，如果將處理器中的所有模塊載入BMC工具，那么狀態(tài)變量眾多，BMC求解過程會遭遇狀態(tài)爆炸問題.因此，需要抽取被測模塊的功能約束，采用抽象技術來簡化其他模塊.

數(shù)值抽象[15]是一種針對數(shù)據(jù)通路中數(shù)值之間關系而提出的抽象技術.在測試處理器的時候，假如某個寄存器的值始終與另外一個寄存器相等，這種關系是恒定不變的，那么這兩個寄存器就需要抽象為一個寄存器.抽象后的系統(tǒng)規(guī)模必定小于原系統(tǒng)的規(guī)模，這樣就縮減了模型規(guī)模，降低了BMC的復雜度.通常，抽象是由給定實際值集作用到抽象域的映射關系達到.然后，將這個映射關系作用到狀態(tài)集以及變遷關系集，進而再生成一個映射關系，但是規(guī)模相對于原系統(tǒng)更小，從而降低了BMC的難度.

具體而言，為了縮減被測模塊的規(guī)模，整個系統(tǒng)按功能被分成若干功能模塊.系統(tǒng)中模塊之間并不是相對獨立的，而是相互協(xié)作的，模塊上游輸出的取值范圍就是該模塊的輸入約束，模塊下游能夠接受的輸入取值范圍就是該模塊的輸出約束.一旦獲得這些約束，待測模塊就被轉(zhuǎn)化為約束模塊，如圖3所示.約束模塊的作用就是控制待測模塊的輸入與輸出，以及替代其他模塊的功能，因此其他模塊就抽象為約束模塊.抽象模塊與待測模塊共同組成了一個功能完備的系統(tǒng)，它等價于原系統(tǒng).

2.2 難測故障的違例抽取激活

在獲得約束模塊后，需要針對BMC產(chǎn)生的性質(zhì)，激活被測電路中的難測故障.如圖2中第2步所示，首先獲得被測電路的難測故障，判斷這個故障集是否為空.如果故障集不空，則逐個從故障集中取出難測故障，編寫激活基于線性時序邏輯(LTL)的性質(zhì).然后，運行BMC工具驗證這條性質(zhì).如果在給定的時間片內(nèi)，BMC工具未能搜索到任何違例，那么性質(zhì)恒成立，難測故障在給定時間片內(nèi)無法被激活；如果性質(zhì)不成立，那么BMC工具將給出一個違例，違反這條性質(zhì).

圖3 約束模塊提取Fig.3 Extraction of constraint component

具體而言，針對被測電路中難測的固定型故障，將激活故障使能條件P恒為否作為驗證性質(zhì)，搜索激活故障的測試序列.例如，圖4展示了一個時序電路，假設該電路的輸出端口存在一個固定為0的故障.為了激活這個故障，需要搜索一個輸入序列，使得輸出值變成1，這就是故障的激活條件P.只需要將激活條件一直為否(G(!P))作為性質(zhì)，與被測電路的模型同時輸入BMC工具，BMC工具將搜索激活該故障的輸入序列.如果在給定時間片內(nèi)，BMC工具未能發(fā)現(xiàn)任何違例，該性質(zhì)恒為真，就不存在激活該故障的測試序列，該故障不可測試；如果BMC工具搜索到一個違例使得性質(zhì)為假(見圖5)，就滿足故障激活條件.只需將違例中輸入序列施加到被測電路輸入端，就可以測試給定故障.

圖4 一個時序電路Fig.4 A sequential circuit

2.3 自測試程序構(gòu)建

SBST方法測試故障的步驟包括觸發(fā)故障和觀測故障導致的響應，因此激活難測故障的違例需要轉(zhuǎn)化為測試該故障的指令序列，而后添加觀測程序形成最終的自測試程序.具體而言，在獲得違例后，抽取違例中的輸入序列，然后將輸入序列映射為測試程序，如圖2所示.映射過程包括兩部分：指令映射和狀態(tài)位設置.指令映射是根據(jù)指令類型和指令控制碼的對應關系，將違例中的輸入序列轉(zhuǎn)化為測試指令或者測試指令序列.狀態(tài)位設置需要通過指令與操作數(shù)協(xié)同來達到，即指令執(zhí)行前一個時間片中設置操作數(shù)，通過指令利用操作數(shù)進行運算，將狀態(tài)位設為給定的值.例如，對于某違例的輸入序列，根據(jù)指令類型和指令控制碼之間的映射關系，該輸入序列被轉(zhuǎn)化為由2條指令構(gòu)成的測試序列.在第1條指令前，添加addi指令以及合適的操作數(shù)，為第1條指令初始化狀態(tài)位的值.同時，為第1條指令準備合適的操作數(shù)，使得這條指令能夠初始化第2條測試指令狀態(tài)位的值，形成一個測試指令序列.然而，這種指令序列只能觸發(fā)難測故障，還不能確保激活該故障的響應可以被觀測.因此，需要為測試指令序列添加相應的觀測指令序列，組成完整的自測試程序.針對難測故障集中的故障，重復上述步驟，逐個產(chǎn)生自測試程序，最終產(chǎn)生GB-SBST程序.

圖5 違例Fig.5 A counterexample

3 GB-SBST方法對Parwan處理器控制模塊的測試

與處理器中的功能模塊相比，控制模塊邏輯復雜，并具有一定的時序深度，很多難測的故障只有特定的測試向量序列才能激活，隨機向量難以確保這些特定的測試向量序列的覆蓋.表1展示多種現(xiàn)有測試方法在Parwan處理器上的故障覆蓋率.雖然基于隨機向量的SBST方法[16]和ATIG方法都測試了Parwan處理器中超過90%的故障，但是它們在控制模塊上的故障覆蓋率都顯著低于全掃描鏈方法所獲得的全處理器故障覆蓋率.這表明基于隨機向量的SBST方法和ATIG方法難以有效地測試復雜的控制模塊，關鍵的控制模塊需要新型的自測試技術.本文擬將GB-SBST方法應用于Parwan處理器的控制模塊，測試難測故障.

表1 現(xiàn)有方法在Parwan處理器上的故障覆蓋率Tab.1 Fault coverage of the existing methods

3.1 Parwan處理器

圖6展示了本方法中Parwan處理器的架構(gòu).Parwan處理器規(guī)模較大，包含了8個主要模塊，分別為累加器(AC)、計算單元(ALU)、移位單元(SHU)、狀態(tài)寄存器(SR)、指令寄存器(IR)、程序計數(shù)器(PC)、地址生成單元(MAR)和控制模塊(CTRL).控制模塊為其他模塊提供控制信號，而且只接收指令寄存器提供的指令，以及狀態(tài)寄存器提供的狀態(tài)信息.

圖6 Parwan處理器架構(gòu)Fig.6 Architecture of Parwan processor

3.2 控制模塊的模型化與精簡

采用門級網(wǎng)表描述的設計需要轉(zhuǎn)化為smv語言描述的設計，才能夠被BMC工具處理.使用Java開發(fā)并完成了一個讀取門級網(wǎng)表邏輯并轉(zhuǎn)化為smv文件的程序，使用該程序?qū)arwan控制模塊的門級網(wǎng)表轉(zhuǎn)化為smv文件.同時，為了避免全處理器進行模型檢測時的狀態(tài)爆炸問題，采用抽象技術，使用處理器中其他模塊施加到控制器的約束來替代它們本身的功能.

首先，對Parwan控制模塊的輸入進行抽象仿真，控制模塊的輸入信號來源共有2個，分別是IR與SR，如圖6所示.SR的輸出為四位CPU狀態(tài)位：V表示溢出位，C表示進位，Z表示零位，N表示負數(shù)位.根據(jù)這些狀態(tài)位的意義，可以得到這些狀態(tài)位之間的約束關系.表2顯示狀態(tài)位之間的約束關系，也是SR對于控制模塊四位輸入的約束情況.當Z為1的時候，N一定為0，且V與C的值相等；當Z等于0時，V的值等于C與N的異或，或者V、C和N的值都等于0.總而言之，這些約束可以由布爾等式來表示，如下所示:

!V*!Z*N+!V*!C*N+V*C*!N+V*!C*!Z*N=1

(1)

對于每一個狀態(tài)位的約束，也可以由以下4組布爾等式表示:

Vout=V*C*!N+V*!C*!Z*N

(2)

Cout=V*C*!N+!V*C*!Z*N

(3)

Zout=V*C*Z*!N+!V*!C*Z*!N

(4)

Nout=!V*!Z*N+V*!C*!Z*N

(5)

表2 SR狀態(tài)位的約束關系Tab.2 Constraints for SR state signals

根據(jù)每個狀態(tài)位的約束，設計約束電路，表示在處理器正常工作模式下，SR對控制模塊施加的影響.將等式(2)～(5)轉(zhuǎn)化為約束電路的門級網(wǎng)表文件,進一步轉(zhuǎn)化為smv文件，施加到控制模塊smv文件的四位輸入狀態(tài)位上.

基于同樣方法將IR的約束轉(zhuǎn)化為對應的約束電路，并使用smv文件表示其約束邏輯，其輸出就作為控制模塊的來自IR的輸入信號，為控制模塊提供合法指令，完成對應的功能.因此，IR的約束電路將約束控制模塊的輸入信號，確保每次輸入都是合法指令.隨后，將SR和IR的約束電路一起施加到控制模塊上.這樣，在進行模型檢測的時候，控制模塊的所有輸入信號值符合原始電路實際輸入，控制模塊在抽象后的模型中是正常工作的，約束模塊等效替換了處理器的其他模塊.由于約束模塊的規(guī)模遠小于處理器中其他模塊的規(guī)模，抽象技術確實成功縮減了被測模型的狀態(tài)數(shù)量.同時，由于有界模型求解問題的計算開銷隨狀態(tài)數(shù)量增大呈指數(shù)型增長，采用抽象技術約簡模型能夠明顯減少測試時間，降低測試成本.

3.3 難測故障對應的違例獲得

在構(gòu)造和簡化被測模塊后，需要針對控制模塊中的難測故障采用BMC工具逐個搜索觸發(fā)序列.本文假設ATIG方法測試Parwan處理器時，控制模塊中未測試到的故障是難測故障.圖7展示了觸發(fā)控制模塊中難測故障的測試程序的示例.首先，根據(jù)未檢測到故障列表的信息，獲得故障對應的門單元、端口信息以及故障類型.假設控制單元中邏輯門U10的A0端口的連接線n19存在固定為1的難測故障，這個故障的激活條件P是導線n19的信號變?yōu)?.其次，將故障激活條件轉(zhuǎn)化成LTL性質(zhì)，采用BMC工具搜索存在違反性質(zhì)的違例.具體而言，將A0端口不可能一直等于1(AG!(n19 == 0))作為性質(zhì).如果在給定的時間片內(nèi)，BMC工具無法找到性質(zhì)的違例，即導線n19的信號恒等于1，難測故障在正常工作模式下不可測試；如果有界模型搜索到違反性質(zhì)的違例，即違例中的輸入序列使得導線n19的信號變成0，那么故障被激活，違例中的輸入序列就是測試該故障的測試序列.通過BMC工具檢測， n19固定為1故障是可測試的.

圖7 獲得違例的過程Fig.7 Process of counterexample generation

基于同樣方法可以測試控制模塊的所有難測故障.表3展示了針對難測故障的BMC工具運行結(jié)果，其中控制模塊有40個難測故障，BMC工具成功地產(chǎn)生了32個故障的違例，但是有8個故障不存在激活它們的違例.這是因為在控制模塊的狀態(tài)機中，這些信號始終保持固定值，它們是不可測試的故障.

3.4 基于違例產(chǎn)生的自測試程序

觸發(fā)難測故障的違例需要轉(zhuǎn)化為測試指令序列，才能執(zhí)行基于軟件的自測試，在線測試控制模塊中的難測故障.根據(jù)第2.3節(jié)，轉(zhuǎn)化過程包括指令映射和狀態(tài)映射.首先，指令映射是指根據(jù)控制碼與指令類型之間的對應關系，將違例中輸入序列轉(zhuǎn)化為指令序列.在Parwan處理器中，控制模塊直接從IR中獲取指令，而且IR約束模塊的輸出等價于IR的輸出，那么違例中IR約束模塊的輸出就是控制模塊的測試指令.這樣，違例中的輸入序列可以轉(zhuǎn)化為指令序列，定義為T：[(Inst1,S1), (Inst2, S2), …]，其中S1,S2, …是每條測試指令的狀態(tài)信號.其次，添加控制指令和相應的操作數(shù)，為下一條指令設置狀態(tài)信號.具體而言，首先增加一條指令和操作數(shù)，設置第1條指令的狀態(tài)信號；然后，為第1條指令添加操作數(shù)，通過第1條指令的運行，為第2條指令設置狀態(tài)信號；最后，繼續(xù)采用這種方式設置指令的狀態(tài)信號，最終得到測試指令序列.

表3 針對難測故障的BMC工具運行結(jié)果Tab.3 BMC results for hard-to-test faults

由圖7可見：在第1個時間片中，違例中IR約束模塊的輸出指令是add，SR約束模塊的輸出狀態(tài)信息(V,C,Z,N)== 0000；在第2個時間片中，違例中輸出指令是and，輸出的狀態(tài)信息是1001.為了觸發(fā)n19固定為0的故障，需要在第1個時間片之前添加一條指令與操作數(shù)，設置指令add的狀態(tài)信號.添加指令“addi 5”就可以將add指令的狀態(tài)位變?yōu)?000.接著，為第1條指令add準備操作數(shù)，通過add指令的加運算，使得ALU運算發(fā)生溢出，并且數(shù)值變?yōu)樨摚瑺顟B(tài)位變?yōu)?001，符合第2條測試指令的狀態(tài)信息.這樣就得到了滿足要求的測試指令序列.最后，本文方法在測試指令序列后添加觀測指令序列，輸出測試結(jié)果與相關符號位，形成難測故障的自測試程序.

4 實驗設計與結(jié)果分析

實驗采用商業(yè)ATPG工具進行故障模擬，獲得故障覆蓋率.圖8顯示了實驗的主要步驟.首先，觸發(fā)指令序列與觀測指令序列組成自測試程序，并且與測試數(shù)據(jù)一起編譯為內(nèi)存文件.然后，將內(nèi)存文件加載到Parwan處理器上，在modelsim工具中進行模擬，并且保存模擬過程中處理器輸入輸出端口值的變化.最后，將值變化文件和Parwan處理器加載到TetraMAX進行故障模擬，并且評估故障覆蓋率.

本文方法主要針對ATIG方法中難測故障，提升現(xiàn)有自測試程序在核心控制模塊中的測試性能，改進后的自測試方法被稱為ATIG+GB-SBST.表4顯示了不同方法在Parwan處理器上的故障覆蓋率結(jié)果.從表4可知，ATIG+GB-SBST方法確實提升了現(xiàn)有自測試方法的測試性能，Parwan處理器的故障覆蓋率達到了95.5%，控制模塊的故障覆蓋率從84.4%提升到了88.9%，解決了28.8%的難測故障.控制模塊中尚未檢測到的故障主要是工作模式下的不可測故障，產(chǎn)生這些故障的原因有以下幾個方面：一方面，處理器的某些導線，在正常工作模式下恒為0(或者恒為1)，不存在激活這些變量上固定為0(或固定為1)故障的測試序列，如表3所示；另一方面，控制模塊中某些導線無法影響任何的輸出信號，進而它們的測試響應無法觀測.

圖8 實驗過程Fig.8 Experiment process

表5顯示了4種不同測試方法的測試開銷.ATIG+GB-SBST方法的全部測試程序包括310條指令，以及775 Byte的數(shù)據(jù).ATIG+GB-SBST方法只需要指令121條，測試數(shù)據(jù)258 Byte.ATIG+GB-SBST方法的總數(shù)據(jù)量比基于隨機向量的SBST方法的數(shù)據(jù)量節(jié)省了36.2%，也少于全掃描鏈方法的測試數(shù)據(jù)量.雖然基于隨機向量的SBST方法、ATIG方法和ATIG+GB-SBST方法的測試時鐘周期數(shù)大于全掃描鏈方法，但是這三種方法的測試時間不會超過全掃描鏈方法的測試時間.這是因為這三種方法采用高速的工作時鐘，而全掃描鏈方法采用低速的測試儀時鐘.ATIG+GB-SBST方法僅比ATIG方法少量增加了測試時間，但是相比于基于隨機向量的SBST方法來說依然減少了87.3%，在測試開銷方面提升明顯.ATIG+GB-SBST方法也不需要任何額外的面積開銷，更不需要采用昂貴的外部測試儀.

表4 不同測試方法的故障覆蓋率Tab.4 Fault coverage of different testing methods

表5 不同測試方法的測試開銷Tab.5 Test cost of different testing methods

5 結(jié)語

處理器中核心的控制模塊由于結(jié)構(gòu)復雜，并且時序深度較大，現(xiàn)有方法難以有效進行測試.本文設計了一種基于BMC的門級自測試方法，有效地測試了控制模塊中的難測故障.這種方法利用抽象技術，將控制模塊的輸入約束替代處理器中的其他模塊，從而簡化了被測處理器.然后，將難測故障轉(zhuǎn)化為LTL性質(zhì)，利用BMC工具搜索觸發(fā)難測故障的輸入序列.最后，將這些違例中的輸入序列轉(zhuǎn)化為測試序列，并添加控制和觀測指令，形成自測試程序.實驗結(jié)果表明，本文方法提高了控制模塊中難測故障的故障覆蓋率，提升了現(xiàn)有自測試方法對核心控制模塊的測試性能.