本文選題：現(xiàn)場可編程門陣列 + 集成電路驗(yàn)證��； 參考：《廣西民族大學(xué)》2015年碩士論文

【摘要】：模擬和混合信號電路已經(jīng)廣泛應(yīng)用于電子消費(fèi)、電通訊、電子醫(yī)療等很多領(lǐng)域。但是,在深亞微米設(shè)計(jì)中,物理效應(yīng)可能會破壞常見的數(shù)字抽象化后的電路行為。本文采用混雜系統(tǒng)的方法對模擬和混合信號電路模型進(jìn)行形式化的驗(yàn)證。提出了電路級驗(yàn)證的形式化方法,此方法是基于變遷驗(yàn)證問題的可達(dá)性分析問題,利用非線性常微分方程的改進(jìn)節(jié)點(diǎn)分析模型對電路的動力學(xué)行為建模,計(jì)算從給定初始狀態(tài)向前探索能達(dá)到的所有可能的電路行為。模擬電路行為的性質(zhì)確保完全正確的發(fā)現(xiàn)設(shè)計(jì)的缺陷。并針對由非線性常微分方程建模的電路系統(tǒng)的驗(yàn)證需求,提出了一種新的集成電路形式化驗(yàn)證的硬件方法,采用FPGA作為硬件加速部件,加速Coho形式化驗(yàn)證算法的計(jì)算。采用Sysgen工具重新改寫Coho形式化驗(yàn)證算法,將Coho形式化驗(yàn)證算法的求解變成對應(yīng)的硬件電路的設(shè)計(jì)問題,通過設(shè)計(jì)合適的硬件完成形式化驗(yàn)證的計(jì)算。實(shí)驗(yàn)結(jié)果表明,與Coho驗(yàn)證算法的軟件執(zhí)行時間相比,硬件實(shí)現(xiàn)可以獲得10倍左右的性能加速。本研究能夠進(jìn)一步擴(kuò)展Coho的應(yīng)用領(lǐng)域,尤其是擴(kuò)展到以前因?yàn)橛?jì)算性能無法應(yīng)用的領(lǐng)域。
[Abstract]:Analog and mixed signal circuits have been widely used in many fields, such as electronic consumption, electric communication, electronic medicine and so on. However, in deep submicron design, physical effects may destroy common digital abstracting circuit behavior. In this paper, the hybrid system method is used to formalize the simulation and mixed signal circuit models. A formal method of circuit level verification is proposed, which is based on the reachability analysis of transition verification problem. The improved node analysis model of nonlinear ordinary differential equation is used to model the dynamic behavior of the circuit. Calculate all possible circuit behaviors that can be achieved from a given initial state forward. The nature of analog circuit behavior ensures the correct detection of design defects. Aiming at the verification requirement of the circuit system modeled by nonlinear ordinary differential equations, a new hardware method for formal verification of integrated circuits is proposed. FPGA is used as the hardware acceleration component to accelerate the calculation of the formal verification algorithm of Coho. The formal verification algorithm of Coho is rewritten by using Sysgen tool, and the solution of the formal verification algorithm of Coho is transformed into the design problem of corresponding hardware circuit, and the calculation of formal verification is accomplished by designing appropriate hardware. The experimental results show that compared with the software execution time of the Coho verification algorithm, the hardware implementation can achieve about 10 times faster performance. This study can further extend the application of Coho, especially to areas where computing performance can not be applied in the past.
【學(xué)位授予單位】：廣西民族大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TN791

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 王憶;;基于面向特征編程范式的形式化驗(yàn)證技術(shù)的應(yīng)用與研究[J];信息與電腦(理論版);2011年01期

2 楊澤民;范全潤;;硬件設(shè)計(jì)的形式化驗(yàn)證技術(shù)[J];太原師范學(xué)院學(xué)報(bào)(自然科學(xué)版);2007年02期

3 葉俊;譚慶平;李暾;;面向特征編程范式的形式化驗(yàn)證技術(shù)研究綜述[J];計(jì)算機(jī)工程與科學(xué);2010年09期

4 周宏斌,黃連生,桑田;基于串空間的安全協(xié)議形式化驗(yàn)證模型及算法[J];計(jì)算機(jī)研究與發(fā)展;2003年02期

5 韓俊剛;硬件設(shè)計(jì)的形式化驗(yàn)證[J];計(jì)算機(jī)研究與發(fā)展;1991年11期

6 張慧;鄭超美;;安全協(xié)議的形式化驗(yàn)證方法概述[J];計(jì)算機(jī)安全;2007年01期

7 王彥本;;集成電路形式化驗(yàn)證方法研究[J];電子科技;2008年08期

8 黃連生,王新兵,謝峰,楊克;安全協(xié)議形式化驗(yàn)證方法的比較與分析[J];計(jì)算機(jī)工程與應(yīng)用;2001年14期

9 張博穎;;優(yōu)先級頂協(xié)議的形式化驗(yàn)證[J];計(jì)算機(jī)仿真;2007年06期

10 項(xiàng)俊龍;陳傳峰;;安全協(xié)議形式化驗(yàn)證方法綜述[J];信息安全與通信保密;2013年05期

相關(guān)會議論文 前2條

1 吳鈴鈴;周干民;何偉;高明倫;;IP軟核的形式化驗(yàn)證[A];全國第十五屆計(jì)算機(jī)科學(xué)與技術(shù)應(yīng)用學(xué)術(shù)會議論文集[C];2003年

2 郭華;莊雷;;電子商務(wù)協(xié)議的形式化驗(yàn)證方法及FR驗(yàn)證實(shí)例[A];2005年全國理論計(jì)算機(jī)科學(xué)學(xué)術(shù)年會論文集[C];2005年

相關(guān)碩士學(xué)位論文 前9條

1 李小波;龍芯2號功能部件半形式化驗(yàn)證方法的研究與實(shí)現(xiàn)[D];首都師范大學(xué);2006年

2 焦金良;基于多項(xiàng)式模型的高層次形式化驗(yàn)證[D];哈爾濱工程大學(xué);2006年

3 張倩;基于可編程邏輯的硬件平臺的設(shè)計(jì)與形式化驗(yàn)證[D];北京交通大學(xué);2009年

4 張金磊;形式化驗(yàn)證技術(shù)在EDA軟件開發(fā)中的應(yīng)用[D];西安電子科技大學(xué);2011年

5 馬小龍;形式化驗(yàn)證在Office安全中的應(yīng)用研究[D];中國人民解放軍信息工程大學(xué);2005年

6 丁廣泓;集成電路形式化驗(yàn)證的FPGA加速技術(shù)研究[D];廣西民族大學(xué);2015年

7 張澤恩;基于GSTE中的符號仿真設(shè)計(jì)與實(shí)現(xiàn)[D];電子科技大學(xué);2012年

8 林立;基于高階邏輯系統(tǒng)HOL的數(shù)字硬件形式化驗(yàn)證[D];西安電子科技大學(xué);2005年

9 譚力;基于情態(tài)演算的UML形式化驗(yàn)證與OCL約束自動生成研究[D];華東師范大學(xué);2010年

，

本文編號：1879179