查敬芳 白 濤 胡立生

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

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

查敬芳1白 濤2胡立生1

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

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

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

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

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

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

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

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

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

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

1 基本知識

1.1SAT問題

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

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

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

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

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

d. 布爾變量x∈{x1,x2,…,xN}，它的取值域?yàn)閧1,0}，即每個(gè)變量。

1.2決策策略

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

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

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

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

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

2.1算法概述

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

2.2空間裁剪

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

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

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

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

2.3決策

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

圖2 搜索空間分布

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

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

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

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

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

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

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

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

如以下實(shí)例：

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)

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

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

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

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

3 實(shí)例應(yīng)用

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

(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給出了求解的詳細(xì)過程記錄，圖5給出了求解結(jié)果。

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

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

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

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

4 結(jié)束語

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

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

[2] 羅春，楊軍，凌明.基于遺傳算法和覆蓋率驅(qū)動(dòng)的功能驗(yàn)證向量自動(dòng)生成算法[J].應(yīng)用科學(xué)學(xué)報(bào)，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ìn)混合遺傳算法[J].化工自動(dòng)化及儀表，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ò)在點(diǎn)擊故障診斷中的應(yīng)用[J].化工自動(dòng)化及儀表，2010,37(8):59～62.

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

[8] 陳可.核級FPGA軟件驗(yàn)證方法研究[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(修改稿)