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

【摘要】：模擬和混合信號電路已經廣泛應用于電子消費、電通訊、電子醫(yī)療等很多領域。但是,在深亞微米設計中,物理效應可能會破壞常見的數字抽象化后的電路行為。本文采用混雜系統(tǒng)的方法對模擬和混合信號電路模型進行形式化的驗證。提出了電路級驗證的形式化方法,此方法是基于變遷驗證問題的可達性分析問題,利用非線性常微分方程的改進節(jié)點分析模型對電路的動力學行為建模,計算從給定初始狀態(tài)向前探索能達到的所有可能的電路行為。模擬電路行為的性質確保完全正確的發(fā)現設計的缺陷。并針對由非線性常微分方程建模的電路系統(tǒng)的驗證需求,提出了一種新的集成電路形式化驗證的硬件方法,采用FPGA作為硬件加速部件,加速Coho形式化驗證算法的計算。采用Sysgen工具重新改寫Coho形式化驗證算法,將Coho形式化驗證算法的求解變成對應的硬件電路的設計問題,通過設計合適的硬件完成形式化驗證的計算。實驗結果表明,與Coho驗證算法的軟件執(zhí)行時間相比,硬件實現可以獲得10倍左右的性能加速。本研究能夠進一步擴展Coho的應用領域,尤其是擴展到以前因為計算性能無法應用的領域。
[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.
【學位授予單位】：廣西民族大學
【學位級別】：碩士
【學位授予年份】：2015
【分類號】：TN791

【相似文獻】

相關期刊論文 前10條

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

2 楊澤民;范全潤;;硬件設計的形式化驗證技術[J];太原師范學院學報(自然科學版);2007年02期

3 葉俊;譚慶平;李暾;;面向特征編程范式的形式化驗證技術研究綜述[J];計算機工程與科學;2010年09期

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

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

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

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

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

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

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

相關會議論文 前2條

1 吳鈴鈴;周干民;何偉;高明倫;;IP軟核的形式化驗證[A];全國第十五屆計算機科學與技術應用學術會議論文集[C];2003年

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

相關碩士學位論文 前9條

1 李小波;龍芯2號功能部件半形式化驗證方法的研究與實現[D];首都師范大學;2006年

2 焦金良;基于多項式模型的高層次形式化驗證[D];哈爾濱工程大學;2006年

3 張倩;基于可編程邏輯的硬件平臺的設計與形式化驗證[D];北京交通大學;2009年

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

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

6 丁廣泓;集成電路形式化驗證的FPGA加速技術研究[D];廣西民族大學;2015年

7 張澤恩;基于GSTE中的符號仿真設計與實現[D];電子科技大學;2012年

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

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

，

本文編號：1879179