鄒鴻基，李 暾，羅 丹，方雨德

(國防科技大學(xué)計(jì)算機(jī)學(xué)院,湖南 長沙 410073)

1 引言

縮短設(shè)計(jì)周期，降低設(shè)計(jì)成本，提高設(shè)計(jì)生產(chǎn)率，一直是集成電路設(shè)計(jì)面臨的重要挑戰(zhàn)。為應(yīng)對這些挑戰(zhàn)，研究人員提出了多種設(shè)計(jì)方法和設(shè)計(jì)理念，敏捷硬件設(shè)計(jì)方法正是近年來出現(xiàn)的一種新設(shè)計(jì)方法。該方法借鑒敏捷軟件設(shè)計(jì)方法，通過設(shè)計(jì)方法、設(shè)計(jì)工具鏈的革新，使得集成電路設(shè)計(jì)流程變“輕”，以提高設(shè)計(jì)生產(chǎn)率。一些成功案例顯示了該方法強(qiáng)大的設(shè)計(jì)效能[1,2]。

在敏捷硬件設(shè)計(jì)方法中，前端建模主流技術(shù)是依托某種高級程序設(shè)計(jì)語言(如Scala、Python)設(shè)計(jì)領(lǐng)域特定語言DSL(Domain Specific Language)，通過定義支持寄存器傳輸級RTL(Regist-er Transfer Level)建模的端口、寄存器、連線和邏輯單元類等語言機(jī)制，擴(kuò)展現(xiàn)有語言的硬件描述能力，并在運(yùn)行程序時(shí)自動(dòng)生成Verilog或其他格式的RTL電路描述，這種DSL又稱為硬件構(gòu)建語言HCL(Hardware Construction Language)。

HCL運(yùn)行時(shí)生成硬件借鑒了編譯技術(shù)，引入了類似于LLVM(Low Level Virtual Machine)[3]的中間格式。在將HCL描述編譯為中間格式后，可在此基礎(chǔ)上快速地評估各種后端設(shè)計(jì)參數(shù)對設(shè)計(jì)的影響，或圍繞中間格式研究各種設(shè)計(jì)驗(yàn)證技術(shù)，如等價(jià)性檢查、模型檢驗(yàn)、限界模型檢驗(yàn)和測試生成等。上述各種驗(yàn)證技術(shù)所需要的共性技術(shù)是符號模擬，但目前還未有針對敏捷硬件設(shè)計(jì)前端建模的符號模擬支持。

針對該問題，本文以PyRTL DSL[4]為目標(biāo)，設(shè)計(jì)并實(shí)現(xiàn)了一個(gè)符號模擬器，以支持后續(xù)測試生成、限界模型檢驗(yàn)和等價(jià)性檢查等驗(yàn)證技術(shù)的研究。本文主要貢獻(xiàn)為：

(1)探討了基于中間格式的符號模擬方法；

(2)建立了中間格式與可滿足性模理論SMT(Satisfiability Modulo Theory)[5]之間的映射規(guī)則；

(3)為敏捷硬件設(shè)計(jì)形式化驗(yàn)證構(gòu)建了基礎(chǔ)。

本文給出的方法不局限于PyRTL，還可遷移到任何中間格式上，例如FIRRTL[6]、CoreIR[7]和LLHD[8]等。

2 背景

2.1 PyRTL簡介

PyRTL是由加州大學(xué)圣巴巴拉分校體系結(jié)構(gòu)實(shí)驗(yàn)室基于Python設(shè)計(jì)的一種硬件設(shè)計(jì)DSL。PyRTL在Python的基礎(chǔ)上提供了一組RTL級建模的原語，以支持精準(zhǔn)的設(shè)計(jì)描述，利用設(shè)計(jì)模式技術(shù)提高設(shè)計(jì)建模的效率。它要求所有邏輯都是同步和可綜合的，也是一種基于執(zhí)行的設(shè)計(jì)構(gòu)建語言。PyRTL的目標(biāo)是簡單、易用和可擴(kuò)展，支持RTL級設(shè)計(jì)描述、模擬、測試與跟蹤等。目前，PyRTL支持與Xilinx PYNQ的集成，便于快速開發(fā)片上系統(tǒng)SoC(System on Chip)原型。

PyRTL設(shè)計(jì)背后的主要?jiǎng)訖C(jī)是通過一組Python類幫助用戶精確地描述數(shù)字硬件結(jié)構(gòu)。為了實(shí)現(xiàn)簡單性和清晰性，PyRTL有意將用戶限制在一組合理的數(shù)字設(shè)計(jì)實(shí)踐中。例如，時(shí)鐘和復(fù)位信號是隱式的，默認(rèn)情況下塊內(nèi)存是同步的，不存在未驅(qū)動(dòng)或高阻抗?fàn)顟B(tài)，不允許未注冊的反饋，等等。這樣，任何以有效代碼表示的設(shè)計(jì)總是與可綜合的硬件相對應(yīng)。

PyRTL提供了WireVector數(shù)據(jù)結(jié)構(gòu)來構(gòu)建邏輯單元之間的連線，共有5種不同類型的WireVector：Basic、Input、Output、Const和Register。Basic將2個(gè)或多個(gè)不同的邏輯元件連接在一起，Input和Output表示電路的輸入和輸出信號，Const表示電路中的常量，而Register表示寄存器，存儲(chǔ)下一拍的輸出信號值。為支持構(gòu)建復(fù)雜的電路邏輯，WireVector上重載了算數(shù)運(yùn)算符、邏輯運(yùn)算符和比較運(yùn)算符等多種運(yùn)算符。除此之外，PyRTL還提供了concat、concat_list等函數(shù)來支持對WireVector進(jìn)行位操作，提供了Conditional Blocks來支持條件語句，提供了select、mux等函數(shù)來支持選擇操作。

圖1給出一個(gè)簡單的PyRTL電路，描述了一位加法器，它有3個(gè)輸入a、b、c,2個(gè)輸出sum、carrry_out：

Figure 1 adder圖1 加法器

2.2 PyRTL中間格式

PyRTL中間格式的目標(biāo)是為RTL之后的硬件設(shè)計(jì)處理提供一套完整的操作和結(jié)構(gòu)。PyRTL提供了Block和WireVector 2種內(nèi)置的數(shù)據(jù)結(jié)構(gòu)，支持以自底向上的方式構(gòu)建硬件。Block是由基本邏輯單元組成的設(shè)計(jì)，它存儲(chǔ)基本邏輯單元以及它們之間的互連。每個(gè)邏輯單元用一個(gè)LogicNet來表示，每個(gè)LogicNet是一個(gè)4元組，一般形式如下所示：

(operator,parameters,args,dests)

其中，operator表示LogicNet可執(zhí)行的操作，用單個(gè)字符表示；parameters表示LogicNet完成操作時(shí)，除輸入信號外可能需要的額外參數(shù)，這些參數(shù)不能在運(yùn)行時(shí)更改；args表示LogicNet的輸入信號集；dests表示LogicNet的輸出信號集。

PyRTL中間格式定義了一些基本的LogicNet操作，如下所列：

(1)邏輯運(yùn)算和算術(shù)運(yùn)算：如加減、與或等，按其標(biāo)準(zhǔn)定義執(zhí)行指定的算術(shù)或邏輯運(yùn)算，每一種運(yùn)算都有2個(gè)參數(shù)。

(2)基本的比較操作：“=”檢查WireVector的每一位是否相等，而“<”和“>”執(zhí)行無符號算術(shù)比較。所有比較操作的輸出是位寬為1的WireVector。

(3)w和n運(yùn)算：w是一個(gè)沒有邏輯函數(shù)的緩沖區(qū)，而n為非運(yùn)算。

(4)x運(yùn)算：表示一個(gè)多路選擇器，含3個(gè)參數(shù)，第1個(gè)參數(shù)是1位選擇信號(select bit)，如果第1個(gè)參數(shù)的值為0，選擇第2個(gè)參數(shù)；如果為1，選擇第3個(gè)參數(shù)。

(5)c運(yùn)算：為concat操作符，將任意數(shù)量的線向量(a0,a1,…,an)拼接成一個(gè)新的WireVector，其中a0為最高位，an為最低位。

(6)s運(yùn)算：為選擇操作符，它根據(jù)指定的常量參數(shù)，選擇WireVector的一個(gè)子段。

(7)r運(yùn)算：代表一個(gè)寄存器，在時(shí)鐘上升沿，它將值從輸入復(fù)制到寄存器的輸出。

(8)m運(yùn)算：代表內(nèi)存的一個(gè)讀取端口，它支持異步或同步讀取。

(9)@運(yùn)算：代表內(nèi)存的一個(gè)寫端口，支持同步寫。

圖2為圖1中間格式對應(yīng)的電路圖。

Figure 2 Circuit diagram圖2 電路圖

圖2中，a、b、c對應(yīng)圖1中定義的輸入，sum和carry_out對應(yīng)圖1中定義的輸出；tmp1=a∧b，tmp2=tmp1∧c，sum=tmp2，對應(yīng)圖1中的sum<<=a∧b∧c；tmp3=a&b，TEMP1=tmp3，對應(yīng)圖1中的temp1<<=a&b；tmp4=a&c，tmp0=tmp4，對應(yīng)圖1中的temp2<<=a&c；tmp5=b&c，對應(yīng)圖1中的temp3=b&c；tmp6=TEMP1∧tmp0，tmp7=tmp5∧tmp6，carry_out=tmp7對應(yīng)圖1中的carry_out<<=temp1|temp2|temp3。

3 符號模擬器設(shè)計(jì)

模擬是集成電路設(shè)計(jì)驗(yàn)證常用技術(shù)之一，對集成電路進(jìn)行模擬時(shí)，首先建立電路模擬模型，然后注入模擬激勵(lì)以激活電路模擬模型，通過運(yùn)行模擬程序驗(yàn)證該模型。通常輸入的模擬激勵(lì)是0、1這樣的二進(jìn)制值。模擬算法通常分為事件驅(qū)動(dòng)的模擬方法和基于節(jié)拍(cycle-based)的模擬方法。

3.1 主要原理

符號模擬仍是一種模擬驗(yàn)證方法，但其接收的模擬激勵(lì)不僅是具體的值，還包含符號。符號模擬的主要思想是用符號代替具體值作為電路模擬模型的輸入，利用模擬算法，由初始輸入出發(fā)，依次經(jīng)過電路的各個(gè)節(jié)點(diǎn)，計(jì)算出每個(gè)節(jié)點(diǎn)的符號表達(dá)式，直到電路的輸出端，得到由初始符號組成的表達(dá)式，該表達(dá)式是一種體現(xiàn)電路功能的約束函數(shù)。

對組合電路，可從初始輸入開始至最終輸出，將邏輯單元輸入輸出連接起來，形成用初始輸入表示的最終輸出的邏輯函數(shù)。而對時(shí)序電路，則需對電路按一定的節(jié)拍數(shù)展開，得到組合電路后再進(jìn)行處理。而在展開時(shí)序電路時(shí)，需要根據(jù)所使用的模擬算法考慮或忽略邏輯單元的延時(shí)。

本文基于PyRTL中間格式，采用基于節(jié)拍的模擬算法，設(shè)計(jì)并實(shí)現(xiàn)符號模擬器，主要挑戰(zhàn)是如何利用中間格式將電路展開并表示為SMT約束，且能用于其他驗(yàn)證任務(wù)。為處理PyRTL中間格式表示的電路既包含字級信號，又包含位級信號，本文選用了SMTLIB2(Statisfiability Modulo Theories LIBrary 2.x)[9]格式作為轉(zhuǎn)換目標(biāo)。SMTLIB2表示是標(biāo)準(zhǔn)格式，可被遵循該標(biāo)準(zhǔn)的各種SMT求解器求解，如Z3[10]、CVC4[11]和Boolector[12]等。

3.2 算法設(shè)計(jì)

針對PyRTL的中間格式，符號模擬器算法的具體步驟如下所示：

Step1通過Block對象，獲得電路的中間格式。

Step2記錄LogicNet中出現(xiàn)的所有Const類型的常量。

Step3判斷電路類型，如果是組合邏輯電路，跳轉(zhuǎn)到Step 4；如果是時(shí)序邏輯電路，跳轉(zhuǎn)到Step 5。

Step4直接遍歷中間格式保存的每一個(gè)LogicNet，判斷符號是否已定義，再根據(jù)其功能轉(zhuǎn)換成不同的SMT語句，具體轉(zhuǎn)換方法見3.3節(jié)的轉(zhuǎn)換規(guī)則，最后將Step 2中保存的常量轉(zhuǎn)換成SMT語句，一并寫入文件。

Step5對時(shí)序邏輯電路進(jìn)行展開，利用節(jié)拍計(jì)數(shù)對不同周期的同一符號進(jìn)行區(qū)分，得到一個(gè)組合邏輯電路。按Step 4對展開的每一拍電路進(jìn)行轉(zhuǎn)換。

符號模擬器的應(yīng)用方法如圖3所示。

Figure 3 Symbolic simulation process圖3 符號模擬過程

算法Step 1中，如前所述，所有的LogicNet及其連接關(guān)系都保存在Block對象中，因此可以從對應(yīng)的Block對象中得到設(shè)計(jì)中包含的所有邏輯單元，以及邏輯單元之間的連接關(guān)系。

算法的核心在Step 4，需要將電路從PyRTL的中間格式轉(zhuǎn)換為SMTLIB2格式，以便于后續(xù)使用。這種轉(zhuǎn)換需要按照LogicNet邏輯運(yùn)算含義，按一定規(guī)則轉(zhuǎn)換為SMTLIB2中相應(yīng)的運(yùn)算及其約束表示。

當(dāng)需要進(jìn)行符號模擬的電路為時(shí)序電路時(shí)(算法Step 5)，必須將電路展開，展開后的電路為一個(gè)組合邏輯電路。除了按照轉(zhuǎn)換規(guī)則將電路轉(zhuǎn)換為SMTLIB2格式外，還需要為電路中的信號名換名，以區(qū)分不同周期間的同名信號。其換名方法是為信號名增加一個(gè)標(biāo)記，用于標(biāo)識(shí)是第幾拍的信號。

3.3 轉(zhuǎn)換規(guī)則

2.2節(jié)表示LogicNet的4元組可寫成如式(1)所示函數(shù)形式：

dests=operator([parameters],args)

(1)

該函數(shù)表示利用參數(shù)parameters和輸入args執(zhí)行操作operator得到輸出dests，其中parameters為選擇使用。

在SMTLIB2中表達(dá)式用前綴形式表示，格式如式(2)所示：

(opa1a2…an)

(2)

表示對a1,a2,…,an執(zhí)行操作op。

因此，根據(jù)操作語義，可將式(1)中賦值符號右邊部分operator([parameters],args)轉(zhuǎn)化成SMT表達(dá)式，如式(3)所示:

(operatorargs[0]args[1] …args[n])

(3)

而SMT表達(dá)式中的等號可表示為:

(=ab)

(4)

綜合式(3)和式(4)，可知式(1)轉(zhuǎn)化為SMT表達(dá)式的規(guī)則如式(5)所示:

(=dests(opargs[0]args[1] …args[n]))

(5)

最后使用assert將此表達(dá)式轉(zhuǎn)換為SMT約束，即在約束求解過程中需被滿足的條件，規(guī)則如式(6)所示：

(assert(=

dests(operatorargs[0]args[1] …args[n])))

(6)

對于LogicNet中無法直接對應(yīng)SMTLIB2的operator，需要使用多個(gè)SMTLIB2的操作op進(jìn)行轉(zhuǎn)化。由于如式(2)所示的表達(dá)式依然可作為操作數(shù)嵌套使用，因此，多個(gè)操作op可表示成:

(op1(op2a1a2…an)(op3…)… (opn…))

(7)

一般而言，需要用到LogicNet中參數(shù)para-meters的情況主要有以下2種：

(1)利用參數(shù)parameters和輸入args共同得到輸出dests，即parameters也是LogicNet輸入?yún)?shù)之一，按照式(7)的規(guī)則，此時(shí)可將式(6)的輸入args替換為參數(shù)parameters和輸入args的表達(dá)式：

(assert(=dests(op1((op2param[0] …param[n])args[0])((op2param[0] …param[n])args[1]))))

(2)參數(shù)parameters將作為LogicNet輸出之一被修改，此時(shí)，parameters的功能與情況(1)中的dests一致。此時(shí)，可在將式(1)轉(zhuǎn)換為式(5)之外，再增加一條約束，規(guī)則同式(5)，如下所示：

(assert(=parameters(operatorargs[0] …args[n])))

對LogicNet轉(zhuǎn)換的關(guān)鍵是對其operator的轉(zhuǎn)換，經(jīng)對比operator與SMT中運(yùn)算的語義，本文給出operator的轉(zhuǎn)換規(guī)則，如下所示：

(1)當(dāng)operator為&、|、∧、n、+、-、*、=、<、>、c時(shí)，參數(shù)parameters為空，args的長度為2，dests的長度為1，具體含義為dests[0] =args[0]opargs[1]。故此時(shí)生成的SMT約束為:

(assert(=dests[0] (opargs[0]args[1])))

(2)當(dāng)operator為～、w、r時(shí)，參數(shù)parameters為空，args的長度為1，dests的長度為1，具體含義為dests[0] =opargs[0]。故此時(shí)生成的SMT語句為：

(assert(=dests[0] (opargs[0])))

注意，r表示寄存器單元，表示前一個(gè)周期的args[0]與當(dāng)前周期的dests[0]相等，因此需要對符號所在周期進(jìn)行區(qū)分，如寄存器輸入為la，輸出為lb，則在第1個(gè)周期中，生成的SMT約束為(assert(=lb_0la_1))，其中_0和_1分別表示第0拍和第1拍。

(3)當(dāng)operator為x時(shí)，表示一個(gè)多路選擇器，此時(shí)參數(shù)parameters為空，args的長度為3，dests的長度為1。多路選擇器定義的操作為ifargs[0] =0 thendests[0] =args[1] elsedests[0] =args[2]。利用SMT的ite(if-then-else)運(yùn)算，轉(zhuǎn)換后得到的SMT語句為：

(assert(ite (=args[0] #b0)(=dests[0]args[1])(=dests[0]args[2])))

其中#b0表示二進(jìn)制0。

(4)當(dāng)operator為c時(shí)，表示將args中的信號拼接為一個(gè)新信號。引入SMT中的concat后，轉(zhuǎn)換得到的SMT語句為：

(assert(=dests[0] concat (args[0]args[1] …args[n])))

(5)當(dāng)operator為s時(shí)，表示根據(jù)parameters指定的位，將args的某些位挑選出來，再合并為一個(gè)新的WireVector信號。引入SMT的extract操作選擇相應(yīng)的位，((_extractlalb)lc)表示選擇lc[la:lb]位。由于parameters中保存的是選擇的每一位，可以用n個(gè)((_extractparam[i]param[i])args[0])選出所有的位，再利用concat將這些位串聯(lián)起來。此時(shí)，需要注意，WireVector類似于Python中的list，但WireVector中的最低有效位LSB(Least Significant Bit)保存在索引為0處。而在SMT提供的BitVec類型中LSB在最右邊。所以，最后將選擇的所有位合并時(shí)，需要將順序顛倒后再合并，最終轉(zhuǎn)換得到的SMT語句為：

(assert(=dests[0] concat(((_extractparam[n]param[n])args[0])… ((_extractparam[0]param[0])args[0]))))

(6)當(dāng)operator為m時(shí)，它執(zhí)行的是讀存儲(chǔ)器功能，參數(shù)parameters為一個(gè)元組，包含2個(gè)引用，一個(gè)是內(nèi)存端口memid，另一個(gè)是對包含該端口的內(nèi)存實(shí)例的引用mem。此時(shí)args的長度為1，dests的長度為1。

引入SMT的Array類型來表示存儲(chǔ)器，定義為：

(declare-constmem(Array(_BitVecm)(_BitVecn)))

其中_BitVecm定義一個(gè)m位的_BitVec，mem為存儲(chǔ)器的符號，m為存儲(chǔ)器的地址位數(shù)，n為存儲(chǔ)單元的位數(shù)。對于讀存儲(chǔ)器，可以利用select操作處理，轉(zhuǎn)換得到的SMT語句為：

(assert(=(selectmemargs[0])dests[0]))，表示dests[0] =mem[args[0]]。

(7)當(dāng)operator為@時(shí)，它執(zhí)行的是寫存儲(chǔ)器功能，參數(shù)parameters為一個(gè)元組，包含2個(gè)引用，一個(gè)是內(nèi)存端口memid，另一個(gè)是對包含該端口的內(nèi)存實(shí)例的引用mem。此時(shí)args的長度為3，分別為存儲(chǔ)地址、數(shù)據(jù)和寫使能信號，dests的長度為0。只有寫使能為高電平時(shí)，才能對存儲(chǔ)器進(jìn)行寫入。引入SMT的store操作進(jìn)行轉(zhuǎn)換，最終得到的SMT語句為：

(assert(ite (=args[2] #b1)(=(storeargs[0]args[1])mem)(=memmem)))

其中#b1表示二進(jìn)制1。

具體含義為：if 寫使能 =1 thenmem[args[0]] =args[1] elsemem=mem。

(8)PyRTL支持提前定義一個(gè)存儲(chǔ)器ROM。此時(shí)，存儲(chǔ)器的數(shù)據(jù)存儲(chǔ)由用戶設(shè)定，存儲(chǔ)在rom_blocks中。因此，將帶有ROM的電路轉(zhuǎn)換為SMT約束時(shí)，還需要利用類似寫存儲(chǔ)器的方法對ROM初始化，此時(shí)就沒有寫使能，直接利用store操作進(jìn)行，如(assert(=(storeaddrdata)rom))，把rom_blocks中所有的數(shù)據(jù)轉(zhuǎn)換為SMT語句。

以圖1的加法器電路為例，由于加法器是組合邏輯電路，直接按照轉(zhuǎn)換規(guī)則，得到的SMT語句如下所示：

1 (declare-consttmp2 (_ BitVec 1))

2 (declare-consttmp1 (_ BitVec 1))

3 (declare-constc(_ BitVec 1))

4 (assert(=tmp2 (bvxortmp1c)))

5 (declare-constsum(_ BitVec 1))

6 (assert(=sumtmp2))

7 (declare-constcarry_out(_ BitVec 1))

8 (declare-consttmp7 (_ BitVec 1))

9 (assert(=carry_outtmp7))

10 (declare-consttmp4 (_ BitVec 1))

11 (declare-consta(_ BitVec 1))

12 (assert(=tmp4 (bvandac)))

13 (declare-consttmp0 (_ BitVec 1))

14 (assert(=tmp0tmp4))

15 (declare-consttmp6 (_ BitVec 1))

16 (declare-constTEMP1 (_ BitVec 1))

17 (assert(=tmp6 (bvorTEMP1tmp0)))

18 (declare-constb(_ BitVec 1))

19 (assert(=tmp1 (bvxorab)))

20 (declare-consttmp3 (_ BitVec 1))

21 (assert(=tmp3 (bvandab)))

22 (assert(=TEMP1tmp3))

23 (declare-consttmp5 (_ BitVec 1))

24 (assert(=tmp7 (bvortmp6tmp5)))

25 (assert(=tmp5 (bvandbc)))

第1～3行定義3個(gè)1位的BitVec變量tmp1、tmp2、c。第4行表示tmp2 =tmp1 ^c，對應(yīng)圖2中用橢圓標(biāo)記的異或門。

4 實(shí)現(xiàn)與實(shí)驗(yàn)結(jié)果

本文利用Python實(shí)現(xiàn)了符號模擬算法，約700行代碼，并已集成到PyRTL中(本項(xiàng)目已開源到GitHub,地址為https://github.com/zou-sheng/PyRTL)。目前，已實(shí)現(xiàn)的符號模擬器用于模擬激勵(lì)自動(dòng)生成，底層使用Z3求解器，對符號模擬的結(jié)果進(jìn)行求解，得到滿足要求的模擬激勵(lì)。

為驗(yàn)證所實(shí)現(xiàn)的符號模擬器的正確性，本節(jié)在一些設(shè)計(jì)實(shí)例上，以自動(dòng)生成的模擬激勵(lì)為輸入，利用 PyRTL提供的模擬功能，通過對比模擬輸出，來判斷自動(dòng)生成的模擬激勵(lì)是否能恰好在指定節(jié)拍上得到預(yù)期的結(jié)果。

實(shí)驗(yàn)所用的機(jī)器為配備了Intel i5-8250U CPU和2 GB內(nèi)存、操作系統(tǒng)為ubuntu 16.04的計(jì)算機(jī)系統(tǒng)。

實(shí)驗(yàn)電路包括一個(gè)簡單狀態(tài)機(jī)、簡易乘法器、Wallace樹形乘法器，以及128位AES加解密電路。實(shí)驗(yàn)電路性質(zhì)如表1所示。

Table 1 Experimental circuits表1 實(shí)驗(yàn)電路

表1中，簡單狀態(tài)機(jī)有2個(gè)1位輸入信號決定狀態(tài)變化。簡單乘法器有2個(gè)32位輸入表示運(yùn)算數(shù)，以及1個(gè)1位信號reset。Wallace樹形乘法器與簡單乘法器類似，有2個(gè)32位運(yùn)算數(shù)和1個(gè)1位的reset信號，但該乘法器中還提供1個(gè)可配置參數(shù)shifts，表示每個(gè)周期的移位次數(shù)。當(dāng)shifts=1時(shí)，乘法器就變成了簡單加法器；當(dāng)shifts=32時(shí)，只需要1個(gè)周期的延遲即可得到乘法的結(jié)果。AES加解密電路有2個(gè)128位的輸入，分別表示明文和密鑰，還有1個(gè)1位信號reset。

對每個(gè)電路，指定隨機(jī)的輸出結(jié)果，展開指定的節(jié)拍后，通過約束求解生成模擬激勵(lì)。生成模擬激勵(lì)的過程進(jìn)行了多次，取平均耗時(shí)。實(shí)驗(yàn)結(jié)果如表2所示。表2列出了各電路展開的節(jié)拍數(shù)、自動(dòng)生成模擬激勵(lì)的平均時(shí)間。

Table 2 Experimental results表2 實(shí)驗(yàn)結(jié)果

此處需特別說明的是AES加密電路的模擬激勵(lì)生成，將明文和密鑰輸入AES加密電路，經(jīng)過10輪加密得到最終的密文。

(1)如果將明文和密鑰作為符號模擬器的輸入，大約需220.65 s，可以得到符號模擬的結(jié)果。加密過程中的字節(jié)替換和列混淆都需要讀取預(yù)先設(shè)置的存儲(chǔ)器。

(2)如果將密文和密鑰作為符號模擬器的輸入求解明文時(shí)，一些信號唯一對應(yīng)存儲(chǔ)器中的值，而Z3求解器需要逐一對存儲(chǔ)器中的值進(jìn)行測試，所需時(shí)間很長。

(3)如果將這53個(gè)對應(yīng)存儲(chǔ)器值的信號每個(gè)周期的值(共636個(gè))，都作為符號模擬器的輸入，大約需193.35 s，可以求解出正確的明文。

通過對比模擬結(jié)果可知，以表2指定節(jié)拍數(shù)為約束，自動(dòng)生成的模擬激勵(lì)為輸入模擬后，一定能在指定節(jié)拍時(shí)觀察到正確的輸出結(jié)果。由此，本文實(shí)現(xiàn)的符號模擬器是正確的。

5 結(jié)束語

本文介紹了一個(gè)面向敏捷硬件設(shè)計(jì)的符號模擬器的設(shè)計(jì)與實(shí)現(xiàn)，核心工作是PyRTL中間格式至SMTLIB2格式的轉(zhuǎn)換，以及時(shí)序電路展開后的變量命名。目前實(shí)現(xiàn)的符號模擬器較為直接，接下來的研究方向有2個(gè)：(1)加入更多的共性優(yōu)化方法，發(fā)揮SMT求解器能力，使其能處理更大規(guī)模的設(shè)計(jì)；(2)根據(jù)具體應(yīng)用，如限界模型檢驗(yàn)、等價(jià)性檢查進(jìn)行針對性的優(yōu)化。