基于SMT求解器的微處理器指令驗證數(shù)據(jù)約束生成技術(shù)

譚 堅 羅巧玲 王麗一 胡夏暉 范 昊 徐 占

(江南計算技術(shù)研究所 江蘇無錫 214083)

隨著計算機體系結(jié)構(gòu)理論與技術(shù)的迅速發(fā)展、制造工藝水平不斷提升以及集成電路設(shè)計日趨復雜，行業(yè)內(nèi)科研人員設(shè)計實現(xiàn)的處理器邏輯功能變得越來越復雜，對處理器測試驗證質(zhì)量的要求越來越高.為保證處理器功能正確性，硬件設(shè)計人員、驗證人員、系統(tǒng)軟件測試人員甚至用戶都或多或少會承擔著處理器功能與性能的測試驗證任務.指令級功能測試是處理器正確性驗證的重要組成部分，貫穿處理器研制過程中的各個階段，在軟件模擬指令驗證、FPGA(field programmable gate array)實物驗證、硬件模擬仿真驗證以及SoC(system on chip)硅后驗證等階段都需要進行充分驗證；指令級測試方法具有通用性的特點，與具體的處理器類型無關(guān)，在專用處理器與通用處理器研制過程中都需要用到，其實現(xiàn)方法依賴于指令語義、內(nèi)部規(guī)范以及指令上下文等.

在開展指令級功能測試的過程中，我們發(fā)現(xiàn)對于測試方案所要求覆蓋的部分特殊場景，采用現(xiàn)有模擬驗證方法較難達到目的.例如，當需要對單指令的結(jié)果進行各種數(shù)據(jù)類型的遍歷驗證時、在約定浮點操作數(shù)的中間結(jié)果為某特定數(shù)值時、在約定2個操作數(shù)之間滿足特定關(guān)系時尤其是約定輸入操作數(shù)與輸出操作數(shù)之間滿足特定的約束關(guān)系時，采用現(xiàn)有主流的模擬驗證方法[1]通常顯得比較低效.此外，很多的指令功能是隱含一些特定的約束關(guān)系，如加減法、乘法指令運算時存在進、借位情況發(fā)生的可能.這些內(nèi)部關(guān)系對于測試人員來說不直接，部分約束甚至需要處理器設(shè)計人員協(xié)助制定.采用現(xiàn)有模擬方法，在制定測試驗證計劃或者生成測試程序的時候很難全面覆蓋，即使能夠?qū)崿F(xiàn)代價也比較大.以上提及的場景都是比較常見的驗證功能點，要求測試人員必須覆蓋.

面對結(jié)果操作數(shù)與指令內(nèi)部關(guān)系進行約束的驗證場景，如果采用功能模擬測試方法，通常需要測試人員根據(jù)指令的語義模擬出該指令的相反語義，將輸出轉(zhuǎn)換成模擬程序的輸入，反推出指令的輸入操作數(shù)，形成驗證元組數(shù)據(jù)，再根據(jù)驗證數(shù)據(jù)生成相應的指令測試激勵，驗證指令功能正確性.部分指令其實是沒有嚴格意義對應的求反過程的，例如浮點指令，假若存在浮點操作數(shù)A×B=C，但是由于舍入模式等原因，導致數(shù)據(jù)元組A,B,C在很多時候并不滿足C/B=A的關(guān)系.

因此，對于系統(tǒng)測試人員而言，很多的待驗證場景采用現(xiàn)有的功能模擬等手段是比較難以實現(xiàn)的；即使采用算法模擬成功實現(xiàn)，得到驗證數(shù)據(jù)的運行時間通常較長，生成的數(shù)據(jù)量也比較有限.

國內(nèi)外處理器設(shè)計研發(fā)機構(gòu)如Intel，IBM等公司，為滿足處理器特殊約束場景的驗證需求，組織了大量的科學家專門設(shè)計了滿足各自處理器約束建模需求的求解器[2-3].根據(jù)IBM公司官網(wǎng)顯示，以色列海法實驗室研究開發(fā)出了GEC(generation core)，Stocs，Mage等專用求解器[4]，并在此基礎(chǔ)上開發(fā)出了Genesys-Pro[5]，F(xiàn)Pgen[6]等一系列系統(tǒng)，很好地滿足了處理器驗證過程中面臨的各種功能驗證需求.由于這些求解器的實現(xiàn)與處理器內(nèi)部設(shè)計細節(jié)緊密相關(guān)，因此這些專用求解器僅限在公司內(nèi)部以及合作單位進行應用.

由于與設(shè)計緊密關(guān)聯(lián)并且需要參考模型等底層環(huán)境和技術(shù)的支撐配合，目前現(xiàn)有以功能模擬為基礎(chǔ)的系統(tǒng)級測試很難全面覆蓋帶約束的待測場景.很多帶約束的待測場景對系統(tǒng)級測試人員來說是可見的，因此將會使系統(tǒng)測試在功能覆蓋方面存在不足.如果不加以覆蓋，將會導致經(jīng)過系統(tǒng)測試的目標處理器仍然存在設(shè)計錯誤的隱患，這對處理器研制來說是不能容忍的.隨著形式化技術(shù)的快速發(fā)展，我們可以在系統(tǒng)級測試過程中引入形式化方法，對指令約束關(guān)系描述并建模求解.在驗證場景與處理器功能測試覆蓋任務之間建立可靠的技術(shù)橋梁，滿足工程實際需要，提升處理器驗證測試質(zhì)量.

本文首先對一種形式化技術(shù)方法——可滿足模理論(satisfiability modulo theory, SMT)[7]進行簡要介紹；然后提出了一種基于SMT求解器的關(guān)系約束求解技術(shù)，分別從指令結(jié)果操作數(shù)約束、操作數(shù)相互關(guān)系約束、指令內(nèi)部關(guān)系約束以及浮點操作數(shù)約束4個方面，闡述SMT技術(shù)在解決指令功能關(guān)系約束建模需求時的具體實現(xiàn)方法，給出了具體約束建模求解算法；之后，指出了求解過程中存在的常見問題并有針對性地提出了優(yōu)化策略；最后，我們對SMT技術(shù)在指令功能驗證中的應用進行了總結(jié)，對后續(xù)進一步工作進行了展望.

1 可滿足模理論概況

可滿足模理論(SMT)是基于布爾命題可滿足問題(Boolean satisfiability problem, SAT)發(fā)展起來的一種形式化技術(shù).其中SAT求解器能夠判定給定的合取范式(conjunctive normal form, CNF)是否存在可以滿足的模型，即判別是否存在滿足所有給定公式都為真的變量賦值.SAT求解技術(shù)在微處理器RTL(register transfer level)級約束驗證中被廣泛應用.研究人員開發(fā)了很多成熟的SAT求解器；這些求解器被當作一種基礎(chǔ)支撐的問題判定技術(shù)，已經(jīng)廣泛應用于人工智能領(lǐng)域和其他問題求解項目中.SMT技術(shù)是在SAT命題邏輯的基礎(chǔ)上擴充了量詞和項，融合了多種背景知識理論，提升了問題描述能力，擴充了應用求解范圍.

SMT求解器支持用戶定義變量、聲明變量之間約束關(guān)系，將用戶自定義的約束描述自動轉(zhuǎn)換成命題邏輯甚至謂詞邏輯公式，然后通過一定的搜索策略、調(diào)用底層SAT求解器進行問題判定求解；問題可滿足時將給出一個滿足所有約束關(guān)系的隨機模型，對用戶定義的變量進行隨機賦值，否則求解器將反饋問題是不可滿足的.

SMT有很多種具體的、被廣泛使用的求解器，各個求解器之間的背景理論存在差別，因此不同求解器有各自擅長的問題求解領(lǐng)域.其中比較通用的是Alt-Ergo，OpenSMT，veriT，Yices，CVC3/CVC4，Z3等，其中微軟公司的Z3、斯坦福大學和愛荷華州立大學聯(lián)合開發(fā)的CVC4求解器尤為突出.Z3支持比特位向量、整型、實數(shù)、浮點等數(shù)據(jù)類型的變量定義與約束關(guān)系描述.支持空理論、數(shù)組、字符串、線性算術(shù)運算、非線性運算、集合運算、差分邏輯、命題邏輯、謂詞邏輯等運算關(guān)系表達，甚至可以將不同領(lǐng)域的知識進行組合，實現(xiàn)復雜問題的求解[8].CVC4支持實數(shù)和整型的線性算術(shù)運算、數(shù)組、元組、歸納數(shù)據(jù)類型、比特位向量、字符串、等式與未解釋函數(shù)等理論運算[9].SMT求解器強大的表達能力在實際問題的建模與求解方面有著廣泛的技術(shù)前景[10-12].

本文正是利用SMT求解器強大的問題描述能力，對指令功能驗證中存在比較復雜的內(nèi)部約束關(guān)系進行建模.借助SMT求解器自動判斷與可滿足情況下隨機模型生成的能力特征，生成測試驗證數(shù)據(jù)，達到在處理器系統(tǒng)級測試任務中覆蓋復雜場景的目的.

2 基于SMT求解器的指令操作數(shù)約束求解技術(shù)

系統(tǒng)級測試中基于約束的指令功能驗證可通過對指令操作數(shù)施加約束，利用求解器建模驗證是否滿足給定的約定操作數(shù)，生成驗證元組數(shù)據(jù)形成對應的測試激勵，驗證目標機器是否滿足該約束對應的驗證數(shù)據(jù).本節(jié)針對模擬驗證方法不便覆蓋的4種情形，說明采用SMT求解器實現(xiàn)指令功能約束求解技術(shù)的優(yōu)越性.

本文中提及的建模描述以及約束求解實驗是采用Z3求解器，原因是其能夠提供多種語言的支持以及API接口，同時能夠支持描述浮點、整型、比特位等數(shù)據(jù)類型；提供了廣泛的邏輯運算接口，能夠?qū)χ噶罴婕暗降亩喾N微指令行為建模提供很好的支持，同時能夠以字符串的方式對求解結(jié)果進行輸出，方便用戶獲取求解結(jié)果以及后續(xù)數(shù)據(jù)的處理.實驗求解器不僅限于Z3，有資料顯示CVC4最新版本[13-14]已經(jīng)能夠支持浮點類型數(shù)據(jù)，因此也能夠?qū)崿F(xiàn)本文中提到的建模描述實驗的所有過程.

2.1 結(jié)果操作數(shù)約束

模擬驗證方式對于很多指令的結(jié)果操作數(shù)不能直接、高效地進行約束求解.例如無符號乘法指令MULRa,Rb,Rc實現(xiàn)Rc=Ra×Rb的功能，這里3個操作數(shù)均為無符號整型類型.如果用戶需要對Rc進行數(shù)據(jù)類型遍歷，同時限定Rb是大于1的整數(shù).那么需要求解Ra，則需要測試人員模擬出形如Ra=RbOPRc，然后制定相應算法實現(xiàn)求解.然而很多時候存在實現(xiàn)代價太大甚至是無法求解的情形.但這時候采用SMT求解器則很容易表達與求解，因為其背景理論支持各種算術(shù)表達式的約束求解.對于約定Rc≡111，同時要求Rb為大于1的整型數(shù)據(jù)，那么要求解滿足條件的Ra，用戶可以采用如下偽代碼約束表達方式進行描述：

①args[0]=mk_gt(Rb,1);…/*描述Rb>1的約束*/；

②args[1]=mk_mul(Ra,Rb,Rc);…/*描述Rc=Ra×Rb的約束*/；

③args[2]=mk_eq(Rc,const_111); …/*描述Rc≡111的約束*/；

④clause=mk_and(args,3); …/*描述同時滿足上述3個約束*/.

其中mk_gt，mk_mul，mk_eq，mk_and都是SMT求解器算子，Ra，Rb，Rc則是用戶使用SMT求解器API聲明的變量；mk_gt(Rb,1)描述的是Rb>1的約束關(guān)系；mk_mul(Ra,Rb,Rc)描述的是Rc=Ra×Rb的約束關(guān)系；mk_eq(Rc,111) 描述的是Rc≡111的約束關(guān)系.然后將以上3個約束關(guān)系分別賦值給args[0]，args[1]，args[2]子公式中，clause=mk_and(args,3)描述的是將上述3個公式進行合取并賦值給CNF公式clause.

上述結(jié)果操作數(shù)約束偽代碼采用Z3求解器建模描述得到CNF范式以及隨機求解模型結(jié)果如表1所示：

Table 1 Result Operand Constraint CNF Formula and Solution in Z3 Solver表1 結(jié)果操作數(shù)約束Z3建模CNF公式以及求解模型

最后，形成的公式clause表示需要滿足所有3個約束關(guān)系；利用SMT求解器進行求解，求解器在運算過程將始終保持上述3個約束條件，如果有解，則系統(tǒng)將返回滿足所有上述約束條件的一組Ra，Rb，Rc的隨機賦值.

對于其他復雜語義的指令，可以通過增加約束變量以及借助SMT支持的命題邏輯運算符進行描述，實現(xiàn)給定約束的建模描述.

2.2 操作數(shù)之間關(guān)系約束

模擬驗證的方式在對操作數(shù)之間的約束關(guān)系描述時也存在不足之處.例如對測試要求對操作數(shù)之間關(guān)系進行約束.仍然以無符號乘法MULRa,Rb,Rc為例.如對測試數(shù)據(jù)進行約束，要求遍歷Rc的數(shù)值中1的個數(shù)從0～64的所有情況，同時要求Ra或者Rb中1的個數(shù)不能多于Rc中1的個數(shù).這時采用模擬驗證的方式就很難高效地實現(xiàn).

相對而言，采用SMT求解器雖然也是比較復雜但仍然能夠相對方便地進行表述與求解.

用戶可以增加變量N1，N2，…，N64，分別對應Rc中最低n位中1的個數(shù)，可以采用4個步驟實現(xiàn)約束建模：

①args[0]=mk_ite(extract(Rc,0,0),(N1=1),(N1=0)); …/*抽取Rc的第0位進行判斷：如果Rc[0]=為1，則N1賦值為1，否則賦值為0*/；

②args[j]=mk_ite(extract(Rc,i,i),(Ni+1=Ni+1),(Ni+1=Ni));…/*抽取Rc中的第i位判斷：如果Rc[i]=1，則Ni+1賦值為Ni+1，否則Ni+1賦值為Ni*/；

③ …/*依此類推，建立Rc所有的位計數(shù)約束關(guān)系，再分別建立Ra或者Rb的位計數(shù)約束關(guān)系N_Ra[i]*/；

④ 最后args[k]=mk_le(N_Ra[64],N64).

其中mk_ite，extract，mk_le是SMT求解器算子：mk_ite描述的是一種if-then-else的約束關(guān)系；extract實現(xiàn)的是抽取SMT變量的某幾個位的功能；mk_le描述的是一種小于等于的約束關(guān)系.

mk_ite(extract(Rc,i,i),(Ni+1=Ni+1),(Ni+1=Ni))描述的是抽取Rc中的第i個位并進行判斷：如果Rc[i]=1，則Ni+1賦值為Ni+1，否則Ni+1賦值為Ni.

通過上述關(guān)系的描述，系統(tǒng)將合取所有公式集合，形成滿足所有上述約束條件的公式，以此作為求解器的輸入進行約束求解.在約束可滿足時，系統(tǒng)將隨機給出滿足所有子公式約束的模型，測試人員可以根據(jù)模型形成驗證數(shù)據(jù)，并由此生成覆蓋特殊場景的測試激勵.

上述操作數(shù)之間關(guān)系約束偽代碼采用Z3求解器建模描述得到CNF范式以及隨機求解模型結(jié)果如表2所示.為簡化描述，這里僅給出滿足上述條件且在Rc的操作數(shù)位表示法中1的個數(shù)為8的情況.

2.3 指令內(nèi)部關(guān)系約束

如果測試驗證人員關(guān)心計算結(jié)果中是否出現(xiàn)進借位的場景，采用SMT求解也是能夠?qū)崿F(xiàn)該場景約束的表達并求解.本節(jié)以64 b的無符號加法ADDLRa，Rb，Rc為例進行說明.

當約定ADDL操作為無符號長字加法以及所有操作數(shù)的值是無法確定結(jié)果是否存在進位的，因為結(jié)果約束最多就約束了64 b.但是計算時可能發(fā)生Ra+Rb得到的有效位實際上是超過64b的情形.為達到加法進位場景覆蓋驗證的目的，我們繼續(xù)給出這種情況SMT求解器的約束建模過程：

Table 2 The CNF Formula of Relational Constraints Between Operands and Solution in Z3 Solver表2 操作數(shù)之間關(guān)系約束Z3建模CNF公式 以及求解模型

①args[0]=mk_eq(Rc_64,extract(Rc_65,63,0));…/*約束Rc_64與Rc_65的最低64 b相同*/；

②args[1]=mk_eq(Ra_64,extract(Ra_65,63,0));…/*約束擴展源操作數(shù)最低64 b與原始源操作數(shù)相同*/；

③args[2]=mk_eq(Rb_64,extract(Rb_65,63,0));…/*同上*/；

④args[3]=mk_eq(Rc_64,mk_add(Ra_64,Rb_64));…/*分別建立結(jié)果操作數(shù)Rc與未擴展之前的Ra和Rb之間的關(guān)系*/；

⑤args[4]=mk_eq(Rc_65,mk_add(Ra_65,Rb_65));…/*建立擴展之后的結(jié)果操作數(shù)與擴展之后的源操作數(shù)之間仍然需要保持原約束關(guān)系*/；

⑥args[5]=mk_eq(1,extract(Rc_65,64,64));…/*獲取Rc_65的最高位并約定其為1，描述發(fā)生進位約束的情況*/；

⑦args[6]=mk_not(mk_eq(1,extract(Ra_65,64, 64)));…/*獲取Ra_65的最高位并約定其不等于1*/；

⑧args[7]=mk_not(mk_eq(1,extract(Rb_65,64, 64)));…/*獲取Rb_65的最高位并約定其不等于1*/.

其中mk_add是SMT求解器算子，描述的是一種加法運算；mk_not描述的是公式求反運算，mk_eq，extract與2.2節(jié)描述功能相同.

上述操作數(shù)之間關(guān)系約束偽代碼采用Z3求解器建模描述得到CNF范式以及隨機求解模型結(jié)果如表3所示：

Table 3 CNF Formula of Instruction Internal Relationship Constraint and Solution in Z3 Solver表3 指令內(nèi)部關(guān)系約束Z3建模CNF公式以及求解模型

2.4 浮點操作數(shù)約束表示

浮點部件作為處理器的重要部件，再加上浮點數(shù)據(jù)組成特殊性，因此浮點運算指令的正確性驗證歷來都是測試驗證的重點.Z3求解器能夠同時支持位、整型、浮點等數(shù)據(jù)類型，另外還支持多種舍入模式，支持半精度、單精度、雙精度、128 b浮點以及其他自定義格式的浮點運算，并且支持IEEE-754 2008標準，因此可使用Z3求解器靈活構(gòu)建多種測試需求的浮點運算約束求解模型.

對浮點操作數(shù)約束通常存在2種方式：第1種是直接通過求解器接口構(gòu)建不同類型的浮點數(shù)據(jù)類型，例如正負零、規(guī)格化數(shù)、非規(guī)格化數(shù)、無窮大以及非數(shù)等；第2種是采用位方式分別構(gòu)建浮點的符號位、指數(shù)位與尾數(shù)位，然后通過拼接以上3部分形成需要驗證的浮點數(shù)據(jù)，如首先拼接成64 b的長整型數(shù)據(jù)，然后采用內(nèi)部接口轉(zhuǎn)換成浮點數(shù)據(jù)類型，通過約束符號位、指數(shù)位、尾數(shù)位的方式實現(xiàn)浮點數(shù)據(jù)約束的目的.結(jié)合前述分析以及對浮點結(jié)果操作數(shù)的約束覆蓋需求，采用模擬驗證方式也是存在不足的.

以雙精度浮點加法運算FADDD為例，假設(shè)測試人員需要驗證舍入模式為向零舍入、浮點加法結(jié)果操作數(shù)的尾數(shù)為0x123456的非規(guī)格化數(shù)且輸入操作數(shù)都是規(guī)格化數(shù)的情況.我們繼續(xù)以偽代碼方式給出這種驗證需求時采用SMT求解器的約束建模過程：

①args[0]=mk_fp_normal(x);…/*約束第1個輸入操作數(shù)為規(guī)格化數(shù)*/；

②args[1]=mk_fp_normal(y);…/* 約束第2個輸入操作數(shù)為規(guī)格化數(shù)*/；

③args[2]=mk_fp_subnormal(x_plus_y);…/*約束輸出操作數(shù)為非規(guī)格化數(shù)*/；

④args[3]=mk_eq(x_plus_y,mk_fp_add(mk_fp_rtz,x,y));…/*約束輸出操作數(shù)x_plus_y等于x與y在舍入模式為向零舍入下的浮點加法運算結(jié)果*/；

⑤args[4]=mk_eq(x_plus_y,mk_fpa_to_fp_bv(mk_concat(sign_x,mk_concat(exp_x,mant_x)),dp_sort));…/*約束將sign_x,exp_x,mant_x進行拼接并形成dp_sort類型的浮點數(shù)據(jù)，同時進一步約束拼接之后的結(jié)果等于x_plus_y*/；

⑥args[5]=mk_eq(mant_x,mk_unsigned_int64(0x123456,bv_sort(52)));…/*約束尾數(shù)為操作數(shù)0x123456*/；

⑦clause=mk_and(6,args);

最后對前6個約束進行與運算，即同時滿足以上6個約束，形成公式clause作為求解器的輸入進行約束求解.對應的Z3建模過程以及求解結(jié)果如表4所示:

Table 4 CNF Formula of Float-Point Instruction FADDD Constraint and Solution in Z3 Solver表4 浮點指令FADDD約束的Z3建模CNF 公式以及求解模型

通過以上4種典型情況的展示，測試人員可基于該技術(shù)進一步擴展并解決絕大多數(shù)計算類指令操作數(shù)約束測試覆蓋的驗證求解需求.在解決約束表達與求解的問題之后，測試人員則可以將更多的時間精力放到測試場景的構(gòu)建中，確保覆蓋更多、更特殊情況的測試場景，提高測試針對性和測試質(zhì)量，有效提升測試覆蓋率.

3 求解優(yōu)化技術(shù)

采用SMT對測試場景進行約束建模與求解的過程中，往往會遇到約束遍歷求解耗時較長的問題，尤其是在涉及較多約束變量、關(guān)系較為復雜的情況下，求解時間可能會非常長.

在指令約束建模編碼的實踐過程中，通過SMT技術(shù)建立的求解程序通常是由若干個子問題的求解過程組成.而單次求解是1個單線程串行計算過程.當某個求解耗時很長甚至時無解時，求解器可能長時間懸掛在某一次求解的情況，導致后續(xù)求解必須等待前面的求解結(jié)束之后才能繼續(xù)的問題.經(jīng)過作者分析與實踐，發(fā)現(xiàn)很多求解器都提供了超時終止求解的功能.針對該問題，SMT用戶在構(gòu)建求解框架時，通過設(shè)定時間閾值，系統(tǒng)將在求解開始之后進行計時，若給定時間耗費完之后仍然不能判定出問題是否可滿足時，系統(tǒng)將終止本次求解過程；轉(zhuǎn)而繼續(xù)后續(xù)的求解判定.這樣就可以避免整個求解模型掛死在單個無效問題求解的情形.通過實現(xiàn)參數(shù)化框架，用戶可以根據(jù)模型求解的特征，對不同的約束模型設(shè)定不同的時間閾值，保證約束求解不會因為時間閾值的限制導致求解質(zhì)量明顯下降.

本文作者還發(fā)現(xiàn)在構(gòu)建遍歷所有約束條件的模型求解程序中，各個子約束求解過程相互之間是松耦合的.通過約束模型求解的合理設(shè)計與組織，不同求解過程是可以拆解成相互獨立的計算過程.這為采用并行化技術(shù)加速整個框架求解提供了可能.作者將耦合度不高的模塊分布到不同的線程，由各個線程并行獨立求解，所有線程求解結(jié)束之后將結(jié)果進行整合，形成統(tǒng)一的約束求解數(shù)據(jù)集合.

本文作者在實踐過程中成功實現(xiàn)了一種基于多進程與多線程相結(jié)合的并行求解框架：頂層使用fork函數(shù)創(chuàng)建多個進程、在單個進程中創(chuàng)建多個線程的方式，實現(xiàn)將原本順序、串行的遍歷約束求解過程分散到N×M個線程中，充分利用當前服務器的計算資源進行問題求解，利用消耗空間資源換取時間，結(jié)合超時終止求解的技術(shù)，采用參數(shù)控制的形式，實現(xiàn)有限時間內(nèi)對指令約束模型的并行求解框架.框架實現(xiàn)流程如圖1所示:

Fig. 1 Schematic diagram of parallel acceleration solution model based on fork and thread technologies圖1 基于fork+thread的并行加速求解模型示意圖

使用4.8.4版本的Z3求解器，在1臺具有2個物理CPU、累計56個邏輯核心、每個核心支持雙線程的Intel服務器上進行實驗，初始時將并行求解框架中進程數(shù)N與線程數(shù)M分別設(shè)置8和4.

同時我們選擇了ADDL、MULL以及邏輯運算指令LOG2XX這3條指令，分別對指令的約束求解模型加速前后的效果進行比較分析.其中ADDL模型相對簡單，求解建模實現(xiàn)時僅有6個約束變量、針對5個約束關(guān)系形成了5個公式，運行過程中單次求解時間相對較短；MULL指令復雜度次之，建模約束個數(shù)較多、求解時間較ADDL長.LOG2XX指令則較為復雜，根據(jù)指令語義每種數(shù)據(jù)類型遍歷的情況下存在16個不同的操作碼，分別定義了8個約束變量，對約束變量建立的約束關(guān)系超過128個，求解時間相對較長.

此外，實驗過程中將單次求解的時間閾值設(shè)置為1 s，即1 s內(nèi)如果約束公式不能判定是否有解則終止，轉(zhuǎn)而對下一約束關(guān)系模型進行求解.如圖2所示，每條指令均選擇了4組數(shù)據(jù)，分別對應了單種約束情況下求解得到1，10，100，1 000組隨機模型的情況.這里的1，10，100，1 000分別對指令的每一個操作數(shù)、每一種操作數(shù)數(shù)據(jù)類型進行完全遍歷時在每種情況下運行的求解次數(shù).需要說明的是，實驗中設(shè)置的每種情況1次隨機模型時，ADDL與MULL對應的模型將累計產(chǎn)生32次有效求解，LOG2XX指令將累計產(chǎn)生超過480次有效求解.3條指令的在串、并行模式下運行求解時的加速比分別如圖2所示:

Fig. 2 Parallel acceleration diagran in 8×4 configuration圖2 在8×4配置下的并行加速示意圖

通過分析，我們看到在累計使用32個線程并行加速的情況下，ADDL在4種情況下實際得到的單次有效求解加速比最高可達6.11，MULL指令模型最大可達12.22，LOG2XX最大可達10.74.數(shù)據(jù)顯示，在相同約束求解模型內(nèi)，隨著求解次數(shù)的增加，總體加速效果越好.盡管沒有達到N×M=32的加速比，但是相比串行順序求解的方式，并行求解模型的加速效果依然非常明顯.

為了進一步獲取更高的加速比，我們調(diào)整N與M的數(shù)值關(guān)系，分別在針對3種指令模型在單種約束情況下得到1 000組隨機求解模型的前提下開展對比試驗，得到的加速效果如圖3所示.從圖3中還可以看到，在支持雙線程的服務器上，采用16×2模式的并行求解框架能夠獲得更好的加速效果.同時也可以看到，不合理的進程數(shù)與線程數(shù)設(shè)置甚至可能起不到加速的效果，并且在3種指令模型求解加速效果均支持這個結(jié)論.因此應根據(jù)實際的服務器配置采用不同的進程數(shù)與線程數(shù)的設(shè)置，達到更快生成指令驗證元組數(shù)據(jù)的效果.

Fig. 3 Parallel acceleration diagram in multiple configurations圖3 多種配置下的并行加速示意圖

綜上所述，通過比較3種指令約束模型的求解時間，我們看到復雜模型的求解時間較長，在約束復雜度相同的情況下，求解時間基本與求解數(shù)目成線性關(guān)系；不同模型之間，復雜度較大的模型加速效果較為明顯；初步結(jié)論顯示，隨著約束模型的復雜度增加和求解次數(shù)增多，采用合理進程數(shù)與線程數(shù)配置的并行求解模型可得到較為理想的加速效果.

4 結(jié)論與未來工作

基于模擬驗證的指令功能測試方法在結(jié)果操作數(shù)約束、操作數(shù)之間的約束、指令內(nèi)部約束以及浮點操作數(shù)約束情形中存在不足，我們提出了一種基于SMT求解器的指令操作數(shù)約束求解技術(shù).針對這4種場景，分別給出了詳細的建模描述過程與求解結(jié)果示意.針對模型求解過程中存在求解時間較長的問題，采用時間閾值機制、超時則終止當前求解的策略；同時利用進程與線程管理技術(shù)，犧牲CPU計算資源換取時間的策略，對指令約束模型實現(xiàn)求解加速.實驗結(jié)果表明，時間閾值策略與合理的進程加線程的并行框架提升了模型求解效率.

根據(jù)本文提出的方法實現(xiàn)生成的測試驗證數(shù)據(jù)與程序，已成功應用于國產(chǎn)神威系列處理器的測試驗證工作中，發(fā)現(xiàn)了一些隱藏較深的設(shè)計問題；同時能夠支持在系統(tǒng)級甚至用戶級層面更加深入地驗證設(shè)計弱項、實現(xiàn)復雜場景的覆蓋，如輔助特殊邊界場景的異常測試驗證.實踐表明，采用SMT指令級約束求解技術(shù)基本能夠?qū)崿F(xiàn)系統(tǒng)級測試指令功能驗證任務中各種場景的建模描述與求解的功能需求，為測試實施人員提供可靠的技術(shù)支撐.

通過與公開報道的IBM，Intel公司關(guān)于指令級功能與數(shù)據(jù)約束求解方面的技術(shù)特征進行比較，利用本文提出的方法與思路基本可實現(xiàn)指令集的功能約束、數(shù)據(jù)路徑約束等主要指令級約束建模求解.同時由于借助了SMT強大的約束表達能力，測試人員甚至可以僅僅根據(jù)設(shè)計規(guī)范說明文檔進行功能與數(shù)據(jù)路徑的約束建模，弱化約束求解對設(shè)計實現(xiàn)的依賴，更加靈活地在處理器系統(tǒng)級測試驗證工作中實現(xiàn)約束求解功能，進一步提升測試質(zhì)量.

在今后的工作中，我們將繼續(xù)探索SMT技術(shù)在復雜約束生成、指令序列約束等驗證場景中的應用前景；進一步探索優(yōu)化約束求解技術(shù)，充分利用現(xiàn)有商用處理器資源，尋找加速模型求解的有效途徑；盡可能在短時間內(nèi)生成更多的驗證測試數(shù)據(jù)，更全面、更高效地滿足處理器研制過程中的功能正確性覆蓋需求，不斷提升處理器系統(tǒng)測試的質(zhì)量.