基于隨機方法和優(yōu)化的DPLL算法的測試用例自動生成技術(shù)研究

查敬芳 白 濤 胡立生

(1.上海交通大學(xué)電子信息與電氣工程學(xué)院，上海 200240；2.深圳中廣核工程設(shè)計有限公司，廣東 深圳 518172)

基于隨機方法和優(yōu)化的DPLL算法的測試用例自動生成技術(shù)研究

查敬芳1白 濤2胡立生1

(1.上海交通大學(xué)電子信息與電氣工程學(xué)院，上海 200240；2.深圳中廣核工程設(shè)計有限公司，廣東 深圳 518172)

提出一種基于隨機方法和優(yōu)化的DPLL算法的測試用例自動生成技術(shù)，并以基于FPGA的核電儀控系統(tǒng)為對象進行了驗證。該方法能驗證HDL描述符合設(shè)計規(guī)范的要求，代碼覆蓋率較好，所提方法在解決大規(guī)模問題時效率有所提升，尤其是對于可滿足性問題，效率提升非常顯著。

測試用例 SAT問題 DPLL算法 核電儀控系統(tǒng)

核電作為一種清潔低碳能源，其經(jīng)濟性好、持續(xù)供應(yīng)能力強，代表著能源優(yōu)質(zhì)化的發(fā)展方向，但是2011年日本福島核電站爆炸事故給人類和環(huán)境造成的破壞也是極其嚴重的。因此，進一步提高核電的安全標(biāo)準(zhǔn)和技術(shù)水平已成為全世界的共識。數(shù)字儀控系統(tǒng)是核電實現(xiàn)可靠性、多樣化設(shè)計的重要手段。而基于FPGA的儀控系統(tǒng)因其開發(fā)和驗證過程的簡便性、系統(tǒng)架構(gòu)的靈活多變性及容錯性等特點，在核電安全重要領(lǐng)域的應(yīng)用比重日益加大，成為實現(xiàn)儀控系統(tǒng)多樣化設(shè)計、定制性設(shè)計的重要手段。而功能驗證的完備性為系統(tǒng)的可靠性提供最直接的保證，為了達到功能驗證的完備性，需要針對測試空間高效率地生成大量的測試用例，盡可能多地覆蓋測試空間中的功能點。

功能驗證中測試用例生成的基本方法有直接測試和隨機測試[1]。直接測試用例擊中的是測試空間中某個特定的功能點，具有單一性和明確的目的性，沒有太多的精簡余地；而隨機測試可以隨機擊中測試空間中的任何一個點。因此，隨機測試是當(dāng)前功能驗證中測試用例生成的主要方法，和直接測試相比，隨機生成的測試用例可覆蓋到測試空間的任一功能點，有可能覆蓋到驗證人員都未想到的功能角落。但也因為這種隨機性，隨機測試有可能導(dǎo)致功能點的重復(fù)覆蓋，這種無謂的重復(fù)就延長了驗證時間，降低了驗證效率。所以，當(dāng)前功能驗證的主要研究熱點是在保證覆蓋率的前提下設(shè)定約束，有效提高驗證效率。這些研究包括：

a. 采用演化計算方法，通過不斷進化，選擇最佳的測試向量[2～4]。

b. 通過分析覆蓋率模型和輸入測試向量之間的關(guān)系建立模型，用優(yōu)化的測試向量驗證收斂過程，如基于貝葉斯網(wǎng)絡(luò)模型的測試方法[5,6]。

c. 研究其他覆蓋率和功能覆蓋率關(guān)系的方法，如通過代碼覆蓋率分析來提高功能覆蓋率[7]。

d. 結(jié)合直接方法和隨機方法生成測試向量，并用路徑覆蓋率衡量驗證工作是否收斂。對于前兩種方法不能覆蓋的邊界情況，將目標(biāo)測試路徑轉(zhuǎn)化為合取范式的可滿足(SAT)問題，用DPLL算法進行求解，以進一步提高路徑覆蓋率[8]。

文獻[8]所提方法很好地解決了在邊界情況下采用隨機方法，覆蓋率提高效率極低的問題，但該方法無法用于解決大規(guī)模問題，這是由傳統(tǒng)的DPLL算法在解決該問題時決策策略部分不足所導(dǎo)致的，因為傳統(tǒng)的DPLL算法的決策策略是每次做決策時重新計算評估函數(shù)，對每個變量的賦值所帶來的影響做出效率評估，非常耗時?；诖?，筆者提出基于隨機方法和優(yōu)化的DPLL算法的測試用例生成技術(shù)。優(yōu)化的DPLL算法在進行決策時僅針對因空間裁剪引起變化的子句進行局部統(tǒng)計，且根據(jù)變量對整個空間的貢獻情況，動態(tài)調(diào)整變量的權(quán)值，從而顯著提高求解效率。

1 基本知識

1.1SAT問題

給定合取范式F，問是否存在變量的某種賦值，使得F的值為真。如果變量存在這樣的賦值，則稱F是可滿足的；如果變量的任意賦值F都為永假式，則稱F是不可滿足的。在人類為大規(guī)模計算問題尋求高效率算法的努力過程中，可滿足問題扮演了重要角色，例如可用于規(guī)劃調(diào)度、對光纖的布線、尋找蛋白質(zhì)的折疊態(tài)以及對計算機芯片進行驗證等[9]。

可滿足問題一般用合取范式來表示，合取范式一般是子句合取的形式，子句則是文字的析取形式，而文字是布爾變量的肯定或者否定形式。其數(shù)學(xué)描述如下：

a. 合取范式F是子句合取的形式，即F=C1∧C2∧…∧Cs，當(dāng)存在變量X使得F=1時，則說明該范式是可滿足的；否則，是不可滿足的；

b. 子句C1,C2,…,CN，其中每個子句是文字析取的形式，即Ci=l1∨l2∨…∨lt，實際上每個子句是一個約束條件；

c. 文字l∈{x1,┑x1，x2,┑x2,…,xN,┑xN}，即每個文字是布爾變量的肯定或者否定形式；

d. 布爾變量x∈{x1,x2,…,xN}，它的取值域為{1,0}，即每個變量。

1.2決策策略

決策賦值是指每次分支選擇時選擇一個變量進行賦值，決策的過程是在未賦值的變量中選擇一個變量進行“0”或“1”的賦值。在DPLL搜索過程中，當(dāng)遇到下面情形之一時，需要在未賦值的變量空間中選擇一個變量進行賦值：無任一單位子句出現(xiàn)，能對變量進行蘊含賦值；而此時又無子句沖突發(fā)生；并且仍有大量子句在當(dāng)前賦值下無法滿足。在遇到上面這3種情形之一時，都需要進行決策賦值。

為了更好地說明筆者提出的決策策略的優(yōu)勢，首先介紹一下已有的常用策略。

最簡單的決策方法是在未賦值的所有變量中隨機選擇一個變量進行賦值。另外一種策略采用啟發(fā)式方法，求當(dāng)前變量狀態(tài)和子句數(shù)據(jù)庫構(gòu)成的復(fù)雜函數(shù)的最大值。在決策時，通過定義評估函數(shù)，對每個變量的賦值所帶來的影響做出效率評估，目前算法所采取的策略可分為兩大類：一類是靜態(tài)的，即在初始情況下，通過為每一個變量賦值，計算它對搜索空間的壓縮程度，然后采用貪心算法，每次選取壓縮效率最高的變量進行隨機賦值。另一類是動態(tài)的，即在每次進行決策時，都利用當(dāng)前的信息重新評估該變量對搜索空間壓縮程度的影響。第1類方法比較快速，一次計算，整個過程都有效，但由于在決策剪枝之后整個空間會發(fā)生變化，每個變量相對于該空間的比值會發(fā)生變化，所以初始的評估不一定有效。第2類方法能解決這個問題，但第2類方法由于每次決策都需要進行重新計算，比較耗時。目前優(yōu)化的算法都采用動態(tài)決策方法，在眾多變量決策策略中，文獻[10]提出的優(yōu)先選取最短子句中出現(xiàn)頻率最大的變量和文獻[11]提出的優(yōu)先選擇最短的正子句這兩種方法比較常用。然而動態(tài)方法在變量數(shù)比較多的情況下，效率很差。

綜上可知，要實現(xiàn)高效率的決策，需要考慮3方面的要求：一是決策算法本身的花費，如果決策算法本身開銷過大，會導(dǎo)致整個算法失去實際意義；二是通過決策分支，能否對整個搜索空間進行優(yōu)化；三是在解決一個問題時所做的決策次數(shù)，決策次數(shù)越少，說明所做的決策越智能。

2 優(yōu)化的DPLL算法

2.1算法概述

筆者所提出的測試用例生成方法結(jié)合了隨機方法和DPLL算法，重點對DPLL算法的決策部分進行優(yōu)化。DPLL算法是解決布爾可滿足性問題的完全算法，該算法是在二叉樹搜索空間中進行深度優(yōu)先的分支搜索。在基本DPLL算法中，核心的4部分是布爾約束傳播、沖突分析、回溯和決策，其中布爾約束傳播、沖突分析和回溯用來裁剪搜索空間，使搜索空間不斷收縮，加快搜索速度。該算法中的另一個重要部分是決策，決策是否智能直接影響總的決策次數(shù)、布爾約束傳播次數(shù)和沖突發(fā)生的次數(shù)，從而影響搜索空間的壓縮程度和搜索效率。筆者所提出的優(yōu)化的DPLL算法流程如圖1所示。

2.2空間裁剪

在筆者所提算法中，選用布爾約束傳播和沖突分析來對搜索空間進行裁剪。

布爾約束傳播是利用單位子句規(guī)則。單位子句是指在當(dāng)前賦值下，除了一個“字”以外，其他文字都已被賦值，且賦值為“0”，稱該子句中未被賦值的這個“字”為單位字。這樣，為了使得單位子句的值為“1”，則該“字”必須賦值為“1”。這樣在搜索中，就不必去搜索值為“0”的分支路徑，就達到了裁剪空間的目的。為了滿足某個單位子句值為“1”而迫使單位字為“1”的過程稱為蘊含，單位字被蘊含賦值后，往往有更多的單位子句出現(xiàn)，于是新的蘊含過程發(fā)生，這種鏈?zhǔn)降奶N含過程就稱為布爾約束傳播。

圖1 優(yōu)化的DPLL算法流程

沖突分析是利用沖突子句的啟發(fā)信息。沖突子句是指在當(dāng)前的賦值下，所有字的值都為“0”的情況下，當(dāng)遇到?jīng)_突子句時，就無需在該路徑上繼續(xù)下去，需要進行回朔，取消部分變量的賦值，回溯到某個層級上，從另外的路徑上重新進行搜索。

2.3決策

優(yōu)化算法的基本思想可用圖2來表示，將整個搜索空間(圖中的大圓形)分成兩部分，未被搜索的不確定空間和已被標(biāo)記的不可滿足空間(圖中的小圓形)，算法的工作就是通過決策選擇被賦值的變量，使得圖中已被標(biāo)記的不可滿足空間變得越來越大，也就是說使得沖突可能發(fā)生的情況提早，在沖突發(fā)生后，經(jīng)過對沖突的分析，將引起沖突發(fā)生的賦值集合加上約束，即對這組賦值集合加上不可滿足的標(biāo)記，使它在之后的搜索過程中不會再出現(xiàn)相同的賦值組合而引起同樣的沖突。那么，隨著已被證明的不可滿足空間越來越大，后續(xù)搜索中未被搜索的空間則相應(yīng)減小，即整個搜索空間的不確定性部分逐漸減小，后續(xù)搜索的工作量相應(yīng)下降，從而使得搜索效率提升。

圖2 搜索空間分布

在該算法中，如何設(shè)定評估函數(shù)選擇優(yōu)先賦值的變量使得不可滿足空間逐漸增大至關(guān)重要?，F(xiàn)有的決策策略思路有：隨機選擇；考慮到文字在最短子句中的信息增益較大，所以優(yōu)先在最短子句中進行選擇；選擇出現(xiàn)頻率最高的文字進行賦值。在前人工作的基礎(chǔ)上，考慮以下兩點選擇評估函數(shù)：出現(xiàn)頻率最高的文字對所有子句的信息增益最大；正負文字出現(xiàn)頻率都高的變量發(fā)生沖突的可能性更大?；谶@兩點，筆者提出一種新的選擇方法，核心思想是：比較所有變量x的正負文字計數(shù)器值h(x)、h(┒x)的大小，選擇二者計數(shù)器值較小的文字為優(yōu)先級構(gòu)建優(yōu)先級隊列，每次選擇隊首的文字對它賦假值。

優(yōu)化的DPLL算法詳細描述如下：

a. 初始情況下，為每個變量x的正、負文字x、┒x各綁定一個計數(shù)器，計數(shù)器值h(x)和h(┒x)都初始化為0。

b. 然后依次將所有子句加入到數(shù)據(jù)庫中，每加一個子句，該子句中相關(guān)文字的計數(shù)器值h(x)或h(┒x)就加1。

c. 比較所有變量x正、負文字計數(shù)器值h(x)、h(┒x)的大小，然后選擇h(x)、h(┒x)中較小的為優(yōu)先級，構(gòu)建優(yōu)先級隊列。

d. 在沖突分析后將學(xué)習(xí)獲得的子句加入數(shù)據(jù)庫時，該子句中相關(guān)文字的計數(shù)器值也加1，同時更新優(yōu)先級隊列。此時再做局部更新，動態(tài)調(diào)整變量對空間的壓縮效率。

e. 決策時，選擇優(yōu)先級隊列隊首的文字，使該文字賦值為“0”。這種賦值方法可使沖突問題更早出現(xiàn)，因為此時選擇的變量是正反文字出現(xiàn)頻率都高的變量，引起沖突的可能性更大。因而可以以此來裁剪空間，使搜索空間逐漸減小，搜索空間中的不確定部分逐漸減少。

f. 在算法的搜索過程中，每個變量的計數(shù)器值會定期用一個正數(shù)值取模，這樣可動態(tài)調(diào)整每個變量對空間貢獻的權(quán)值，使后續(xù)因?qū)W習(xí)子句而產(chǎn)生影響的變量權(quán)值較高，同時防止某些變量長期得不到賦值的情況。

如以下實例：

l1:(┒m∨n∨p)

l2:(m∨p∨q)

l3:(m∨p∨┑q)

l4:(m∨┑p∨q)

l5:(m∨┑p∨┑q)

l6:(┑n∨┑p∨q)

l7:(┑m∨n∨┑p)

l8:(┑m∨┑n∨p)

采用所述的決策策略，該實例表示的優(yōu)先級隊列如圖3所示。

圖3 優(yōu)先級隊列

初始情況下，為每個變量的正、負文字各綁定一個計數(shù)器，即{文字x，計數(shù)器值h(x)}，h(x)初始化為0。如上例，則有{┑m,0}、{m,0}、{n,0}、{p,0}、{q,0}、{┑q,0}、{┑p,0}、{┒n,0}，然后依次讀取子句l1～l8，并更新計數(shù)器值。讀完子句之后，比較變量x相應(yīng)文字的計數(shù)器值h(x)、h(┑x)，選擇計數(shù)器值較小的文字為優(yōu)先級構(gòu)建優(yōu)先級隊列(圖3)。然后在需要做變量決策時，選擇優(yōu)先級隊列隊首的文字，對該文字賦“0”值。在空間裁剪過程中遇到?jīng)_突子句時，在沖突分析和添加學(xué)習(xí)子句之后，動態(tài)更新上述計數(shù)器值，并根據(jù)新的計數(shù)器值調(diào)整優(yōu)先級隊列。

所提決策策略遞歸地生成決策樹，直到判定該問題為可滿足性問題或者總搜索空間都被標(biāo)記為不可滿足的空間為止。原有的方法在生成決策樹的過程中易出現(xiàn)過擬合現(xiàn)象，即在生成決策樹的過程中因為剪枝不充分或者生成決策樹的算法計算“精度”過高，導(dǎo)致生成的決策樹非常復(fù)雜。但優(yōu)化的算法在決策時選擇導(dǎo)致沖突發(fā)生可能性最大的變量進行賦值，逐漸擴大不可滿足空間，使總搜索空間中不確定部分逐漸縮小。

3 實例應(yīng)用

筆者關(guān)注的是基于FPGA的核電儀控系統(tǒng)開發(fā)實現(xiàn)階段之后的功能驗證部分。在根據(jù)要求規(guī)范開發(fā)設(shè)計完基于FPGA的核電儀控系統(tǒng)各個模塊的HDL程序后，就對該系統(tǒng)的各個模塊進行功能驗證。選取其中一個模塊進行示例，該模塊的輸入變量個數(shù)為2 424。首先用隨機方法生成測試用例，將它輸入到系統(tǒng)的該模塊中，然后通過EDA軟件收集覆蓋率。某一時刻，發(fā)現(xiàn)覆蓋率已較高，并且此時輸入隨機方法生成的測試用例，并不能明顯提高覆蓋率，此時將未覆蓋路徑構(gòu)建為布爾可滿足性問題，并化為標(biāo)準(zhǔn)形式，標(biāo)準(zhǔn)形式的子句個數(shù)為14 812，其合取范式的標(biāo)準(zhǔn)表達式列舉如下：

(x450∨┑x1813)

∧(┑x1005∨┑x2160)

∧(┑x481∨┑x495∨x584)

∧(x263∨x1820)

∧(┑x799∨┑x1223)

∧(x701∨x2226)

∧(x801∨┑x1709)

∧(┑x636∨┑x1534)

∧(┑x685∨┑x868)

∧(┑x967∨┑x2396)

∧(┑x1087∨┑x2311)

∧(x1969∨x2218)

∧(┑x1183∨┑x2419)

∧(┑x100∨x1830)

∧(x715∨x1493)

∧(x821∨x1249∨┑x1747∨x2040∨┑x1269∨x2096)

∧(x815∨x825∨x2144∨x1088∨┑x998∨x1841)

?

∧(┑x700∨┑x1389)

∧(x1118∨x1422)

然后用所提算法求解，圖4給出了求解的詳細過程記錄，圖5給出了求解結(jié)果。

圖4 可滿足的大數(shù)據(jù)量測試數(shù)據(jù)的計算過程

圖5 可滿足的大數(shù)據(jù)量測試數(shù)據(jù)的計算結(jié)果

選取表1中的測試數(shù)據(jù)，分別用文獻[8]算法和筆者所提的優(yōu)化算法進行求解，求解所用時間見表1。由表1的對比結(jié)果可知，筆者所提方法可用于解決大規(guī)模問題，并且在解決大規(guī)模問題時效率有所提升。對于可滿足性問題，提升效果非常顯著。更重要的是，當(dāng)所解決的問題是不可滿足性問題時，效率提升也很明顯。文獻[8]算法用于解決不可滿足性問題時，需要遍歷所有空間，時間消耗非常大，并且時間消耗大多數(shù)都是在不可接受的范圍內(nèi)。而筆者所提方法，每次決策都排除了一些已知的不可滿足空間，從而使需要搜索的空間逐漸減小。對于這類問題，筆者所提算法體現(xiàn)出相當(dāng)大的優(yōu)勢。

表1 文獻[8]算法和筆者所提算法的結(jié)果比較

4 結(jié)束語

對于核電這種高安全性重要領(lǐng)域的功能驗證，筆者所提方法能驗證HDL描述符合設(shè)計規(guī)范的要求，代碼覆蓋率較好，且相對于文獻[8]算法，該方法在解決大規(guī)模問題時的效率有所提升，對可滿足性問題提升效果非常顯著，并且當(dāng)所解決的問題是不可滿足性問題時，效率提升也很明顯。

[1] 鐘文楓.SystemVerilog與功能驗證[M].北京：機械工業(yè)出版社，2010.

[2] 羅春，楊軍，凌明.基于遺傳算法和覆蓋率驅(qū)動的功能驗證向量自動生成算法[J].應(yīng)用科學(xué)學(xué)報，2005,23(4):375～379.

[3] Samarah A，Habibi A，Tahar S，et a1．Automated Coverage Directed Test Generation Using a Cell-Based Genetic Algorithm[C].Proceedings of IEEE International High Level Design and Test Workshop.Monterey：IEEE，2006：19～26.

[4] 范小勤，汪小紅，尹潔.約束優(yōu)化問題的改進混合遺傳算法[J].化工自動化及儀表，2010，37(7):13～16.

[5] Fine S，Ziv A．Coverage Directed Test Generation for Functional Verification Using Bayesian Networks[C].Proceedings of the 40th Design Automation Conference.Anaheim：IEEE，2003：286～291.

[6] 王豪，鄭恩讓.概率神經(jīng)網(wǎng)絡(luò)在點擊故障診斷中的應(yīng)用[J].化工自動化及儀表，2010,37(8):59～62.

[7] 傅亮，盧鼎，張志敏，等.通過分析代碼覆蓋提高功能覆蓋率的驗證輸入自動生成方法[J].計算機輔助設(shè)計與圖形學(xué)學(xué)報，2009,21(4):454～460.

[8] 陳可.核級FPGA軟件驗證方法研究[D].上海：上海交通大學(xué)，2014.

[9] Gomes C P，Selman B.Satisfied with Physics[J].Com-puter Science,2002,297(5582)：784～785.

[10] Jeroslow R G,Wang J C.Solving Propositional Satisfiability Problem[J].Annals of Mathematics and Artificial Intelligence, 1990,1(1):167～187.

[11] Jing M E, Zhou D, Tang P S.Solving SAT Problem by Heuristic Polarity Decision-making Algorithm[J].Science in China Series F: Information Sciences,2007,50(6):915～925.

ResearchofAuto-generationTechnologyofTestCasesBasedonRandomMethodsandOptimizedDPLLAlgorithm

ZHA Jing-fang1, BAI Tao2, HU Li-sheng1

(1.SchoolofElectronicInformationandElectricalEngineering,ShanghaiJiaotongUniversity,Shanghai200240,China;2.ChinaNuclearPowerEngineeringDesignCo.,Ltd.,Shenzhen518172,China)

The random methods and optimized DPLL algorithm-based auto-generation technology for the test cases was proposed. Taking FPGA-based instrument and control system in the nuclear power generation as the object of test to show that this HDL specifications can meet design requirements along with better code coverage; and the efficiency of the proposed method is improved in solving large-scale issues; and regarding the satisfiability, the efficiency promotion is significant.

test cases, SAT issue, DPLL algorithm, instrument and control system in nuclear power generation

TP206

A

1000-3932(2016)09-0927-06

2016-07-12(修改稿)