丁廣泓　吳麗佳

摘要摘要：OpenCoho是一個(gè)通過可達(dá)性分析及計(jì)算對(duì)集成電路設(shè)計(jì)進(jìn)行形式化驗(yàn)證的軟件工具。它可以驗(yàn)證由非線性常微分方程建模的電路系統(tǒng)的正確性。提出基于FPGA的驗(yàn)證算法硬件加速方法，探討環(huán)形振蕩器電路有效性驗(yàn)證，通過仿真說明該方法的可行性和意義。實(shí)驗(yàn)結(jié)果表明，利用該方法平均驗(yàn)證速度提高了約10倍。

關(guān)鍵詞關(guān)鍵詞：形式化方法；集成電路驗(yàn)證；OpenCoho；FPGA

DOIDOI：10.11907/rjdk.151218

中圖分類號(hào)：TP303

文獻(xiàn)標(biāo)識(shí)碼：A文章編號(hào)文章編號(hào)：16727800（2015）004005203

0引言

隨著電路設(shè)計(jì)復(fù)雜度的不斷增強(qiáng)，電路驗(yàn)證的重要性日益突出。然而，傳統(tǒng)驗(yàn)證方法不能涵蓋系統(tǒng)所有可能出現(xiàn)的問題。形式化驗(yàn)證方法可以對(duì)其功能進(jìn)行詳細(xì)驗(yàn)證，越來越受到關(guān)注。

對(duì)于同時(shí)包含離散分量與連續(xù)分量的數(shù)字電路，要將驗(yàn)證的問題公式化，可以通過可達(dá)性分析解決。這種電路可以用常微分方程建模，將電路驗(yàn)證問題等價(jià)于計(jì)算常微分方程模型的可達(dá)狀態(tài)集和檢驗(yàn)電路在這些狀態(tài)的屬性。

OpenCoho是一個(gè)可以驗(yàn)證模擬或混合信號(hào)電路性質(zhì)的形式化驗(yàn)證軟件工具[2]（簡(jiǎn)稱Coho）。其特點(diǎn)如下：①使用常微分方程來近似電路系統(tǒng)；②可以應(yīng)用于非線性的電路模型[2]；③可以有效處理復(fù)雜度高的問題。Coho已經(jīng)應(yīng)用于Van der Pol振蕩器、Yuan-Svensson觸發(fā)器、Rambus環(huán)形振蕩器、異步電路等典型電路。

本文介紹Coho驗(yàn)證電路性質(zhì)的一般流程、探討利用System Generator[4]來加速Coho的核心模塊Mode的方法和技術(shù)[3]、描述Mode的硬件設(shè)計(jì)[5]，驗(yàn)證環(huán)形振蕩器電路的有效性，并對(duì)結(jié)果進(jìn)行對(duì)比分析，最后得出結(jié)論。

1Coho

1.1形式化驗(yàn)證

形式化模型是使用數(shù)學(xué)形式化規(guī)則將特定系統(tǒng)形式化而成的抽象數(shù)學(xué)模型，形式化驗(yàn)證即對(duì)此模型的驗(yàn)證。此方法可以應(yīng)用于硬件系統(tǒng)、軟件系統(tǒng)、網(wǎng)絡(luò)協(xié)議、飛機(jī)系統(tǒng)等。一般來說，其涉及的數(shù)學(xué)模型包括有限狀態(tài)機(jī)、標(biāo)記變遷系統(tǒng)、佩特里網(wǎng)絡(luò)等。

近年來，形式化驗(yàn)證成功應(yīng)用于離散系統(tǒng)數(shù)字電路和通信協(xié)議領(lǐng)域。將形式化驗(yàn)證技術(shù)應(yīng)用領(lǐng)域擴(kuò)展到連續(xù)動(dòng)力學(xué)系統(tǒng)尚具有一定挑戰(zhàn)性。

混雜系統(tǒng)是同時(shí)包含離散行為與連續(xù)行為的動(dòng)力學(xué)系統(tǒng)。在嵌入式系統(tǒng)、飛行控制器和同時(shí)帶有數(shù)字信號(hào)及模擬信號(hào)的電路常用到混雜系統(tǒng)。越來越多的計(jì)算機(jī)成為關(guān)鍵安全系統(tǒng)的自動(dòng)控制器，模擬電路對(duì)深亞微米集成電路的影響日益加大。

一般稱混雜系統(tǒng)的形式化模型為混雜自動(dòng)機(jī)。大部分非線性混雜系統(tǒng)的驗(yàn)證問題是不可判定的。對(duì)這類系統(tǒng)的驗(yàn)證要用到針對(duì)混雜系統(tǒng)的可達(dá)性分析。

1.2相關(guān)知識(shí)

“微分包含”經(jīng)常被用于研究混雜系統(tǒng)。微分包含（ODI）是指具有如下形式的常微分方程（ODE）：

dxdt∈F（x，t）

其中，F(xiàn)（x，t）表示一個(gè)集合，而非實(shí)數(shù)空間中的一個(gè)點(diǎn)。

電路系統(tǒng)一般可以分為模擬電路系統(tǒng)和數(shù)字電路系統(tǒng)。模擬電路系統(tǒng)對(duì)連續(xù)電信號(hào)進(jìn)行處理，數(shù)字電路系統(tǒng)對(duì)離散電信號(hào)進(jìn)行處理。

混雜電路系統(tǒng)指同時(shí)具有連續(xù)動(dòng)態(tài)和離散事件動(dòng)態(tài)行為，且二者之間相互作用的電路系統(tǒng)。由于混雜電路系統(tǒng)是非線性的，其模型用微分包含表示，所以對(duì)混雜電路系統(tǒng)進(jìn)行可達(dá)性研究必須用到近似方法。

過近似常用于可達(dá)性分析，其在保持原空間性質(zhì)不變的基礎(chǔ)上，對(duì)原空間進(jìn)行適當(dāng)擴(kuò)大，使其更適合驗(yàn)證和計(jì)算。

過近似的優(yōu)點(diǎn)是能驗(yàn)證系統(tǒng)的不安全性，如果擴(kuò)大后的空間不滿足安全性，那么原空間一定也不滿足。

1.3Coho及Coho可達(dá)性驗(yàn)證流程

Coho是一個(gè)對(duì)用非線性常微分方程建模的系統(tǒng)進(jìn)行可達(dá)性分析的工具。為了便于計(jì)算，Coho用過近似的方法將每一段的非線性O(shè)DI模型近似成了線性O(shè)DI模型。近似后的模型如下：

直到模型時(shí)間結(jié)束或遇到不可達(dá)情況。

2電路中的系統(tǒng)級(jí)建模

2.1使用System Generator進(jìn)行硬件設(shè)計(jì)

System Generator是一個(gè)借助FPGA硬件設(shè)計(jì)來進(jìn)行系統(tǒng)級(jí)建模的工具。它擴(kuò)展了Simulink的許多功能，使得到的模型更適合硬件設(shè)計(jì)。在傳統(tǒng)軟件設(shè)計(jì)方法中，一般采用Matlab、Java、C語言等來描述各個(gè)功能模塊，進(jìn)而實(shí)現(xiàn)系統(tǒng)建模。如果在寄存器傳輸級(jí)中將Matlab等語言描述經(jīng)人工轉(zhuǎn)換為HDL語言，要求設(shè)計(jì)人員要同時(shí)掌握這兩類語言，而且這個(gè)轉(zhuǎn)換過程會(huì)花費(fèi)大量的時(shí)間和精力，還可能會(huì)產(chǎn)生一些錯(cuò)誤，從而降低了開發(fā)效率。

2.2設(shè)計(jì)流程

圖1描述了System Generator設(shè)計(jì)過程。首先，在Matlab算法中完成系統(tǒng)建模后，通過調(diào)用System Generator將simulink模型轉(zhuǎn)換成硬件可執(zhí)行模型；然后，在Xilinx綜合工具ISE中進(jìn)行布局布線；最后，生成bit流文件并下載到FPGA中，從而完成算法設(shè)計(jì)到硬件的實(shí)現(xiàn)。

3Coho加速設(shè)計(jì)

3.1Coho的系統(tǒng)結(jié)構(gòu)

Coho有兩個(gè)主要組件：一個(gè)使用Matlab編寫，另一個(gè)使用Java編寫。圖2為Coho的系統(tǒng)結(jié)構(gòu)圖。

Matlab組件提供了用戶操作界面，由于需要驗(yàn)證的系統(tǒng)模型被寫成了Matlab的數(shù)據(jù)格式，用戶通過輸入一系列Matlab函數(shù)來操作Coho。這些函數(shù)包括建立模型、定義多面體和計(jì)算可達(dá)區(qū)域。系統(tǒng)模型構(gòu)建與可達(dá)空間模型構(gòu)造也是在Matlab中完成。Java組件的主要功能是計(jì)算投影多邊形和線性規(guī)劃求解。Java組件和Matlab組件通過一個(gè)C程序作為管道進(jìn)行通信。

3.2Mode模塊

Matlab組件中的Mode模塊至關(guān)重要，在Coho中被頻繁調(diào)用。Coho在Mode模塊消耗的時(shí)間占整個(gè)軟件運(yùn)行時(shí)間的40%～45%。Mode模塊的功能是實(shí)現(xiàn)可達(dá)性計(jì)算，根據(jù)每?jī)蓚€(gè)相鄰離散時(shí)間段的多面體是否相交，推斷其是否可達(dá)，進(jìn)而生成軌跡。計(jì)算多面體是否相交[8]，即判斷一個(gè)多面體的頂點(diǎn)中是否至少有一個(gè)在另一個(gè)多面體內(nèi)，其運(yùn)行速度很大程度上影響整個(gè)軟件的性能。Mode模塊因?yàn)樯婕按罅康木仃囘\(yùn)算，所以速度并不理想。

3.3硬件加速M(fèi)ode模塊

圖3是將Mode模塊硬件化的總體設(shè)計(jì)圖。Coho的Matlab組件計(jì)算多面體的頂點(diǎn)后將其輸入到FPGA中，F(xiàn)PGA判斷頂點(diǎn)是否在另一個(gè)多面體內(nèi)，將結(jié)果返回Matlab組件。Mode模塊的功能用System Generator輔助設(shè)計(jì)實(shí)現(xiàn)。設(shè)計(jì)如圖4所示，F(xiàn)1、F2、F3是輸入的激勵(lì)，MCode是判斷點(diǎn)是否在多面體內(nèi)的核心算法單元，其應(yīng)用的Matlab函數(shù)包括多面體每個(gè)面的方程。當(dāng)有輸入進(jìn)入Mcode時(shí)， Matlab函數(shù)根據(jù)輸入的不同對(duì)其進(jìn)行相應(yīng)處理，最后得出結(jié)果。

4實(shí)驗(yàn)與性能分析

4.1實(shí)驗(yàn)環(huán)境

本文在測(cè)試平臺(tái)上實(shí)現(xiàn)了Coho算法加速器。測(cè)試平臺(tái)由一臺(tái)主機(jī)和一塊FPGA算法加速器構(gòu)成，通過PCI-E×8接口相連。主機(jī)配置為Intel四核I5處理器，4.0GB內(nèi)存。硬件加速器是Xilinx公司生產(chǎn)的VC707原型。

環(huán)形振蕩器具有不穩(wěn)定性，電壓在跳變過程中可能會(huì)達(dá)不到要求值，所以驗(yàn)證環(huán)形振蕩器的有效性尤為重要。

選取一個(gè)環(huán)形振蕩器作為實(shí)驗(yàn)對(duì)象，該振蕩器由3個(gè)反相器組成，取各反相器的輸出電壓為偵測(cè)變量，檢測(cè)其有效性。輸出結(jié)果是一維向量，如果向量中的元素是同號(hào)的，表示代表電路模型的多面體相交。當(dāng)系統(tǒng)模型驗(yàn)證結(jié)束時(shí)，如果沒有多面體不相交，則系統(tǒng)模型可達(dá)，即環(huán)形振蕩器有效，否則無效。

4.2FPGA綜合結(jié)果

測(cè)試Coho的Mode模塊在FPGA上的運(yùn)行情況，結(jié)果顯示硬件加速器的計(jì)算結(jié)果與軟件計(jì)算結(jié)果完全一致。

從表1可以看出，相對(duì)于Coho常規(guī)執(zhí)行時(shí)Mode模塊占用的時(shí)間，Mode模塊硬件化可獲得超過10倍的加速效果；并且規(guī)模越大，節(jié)省時(shí)間越多。Coho的整體運(yùn)行時(shí)間將節(jié)約35%～40%。

5結(jié)語

Coho是形式化驗(yàn)證領(lǐng)域的一個(gè)重要軟件平臺(tái)，目前基于通用處理器平臺(tái)的Coho計(jì)算量大。針對(duì)此問題，本文在FPGA的基礎(chǔ)上，對(duì)Coho的可達(dá)性分析算法加速，通過將Coho的核心模塊硬件化，使計(jì)算速度提高了約10倍，并正確驗(yàn)證了一個(gè)環(huán)形振蕩器的有效性。結(jié)果表明，基于FPGA的硬件加速有效提高了Coho的性能，對(duì)形式化方法在混雜系統(tǒng)中的應(yīng)用具有重要意義。

參考文獻(xiàn)參考文獻(xiàn)：

[1]CHAO YAN. Coho a verification tool for circuit verification by reachability analysis[D]. Columbia：University of British Columbia，2006.

[2]CHAO YAN. Formal verification of c-element circuits[C]. Asynchronous Circuits and Systems （ASY NC），2011 17th IEEE International Symposium ，2011： 55-64.

[3]張曉夢(mèng)，張濤.基于FPGA實(shí)現(xiàn)CT圖像重建加速的設(shè)計(jì)[J].液晶與顯示，2014（3）：455-460.

[4]蔣小燕，宗華姣，成旭，等.軟件導(dǎo)刊，2013，12 （7）： 104-105.

[5]宋慶增，張金珠，武繼剛.時(shí)域有限差分算法的FPGA加速技術(shù)研究[J].計(jì)算機(jī)工程與科學(xué)，2013（9）：1-6.

責(zé)任編輯（責(zé)任編輯：陳福時(shí)）