幾十年以來，隨著電子技術(shù)的發(fā)展，微處理器已逐漸成為現(xiàn)代電子設(shè)計中重要且不可或缺的一部分，成為眾多電子設(shè)備的數(shù)字大腦，使今天的數(shù)字化生活方式成為可能。目前的處理器只占用了幾平方厘米的硅芯片，集成化程度高，并能夠以驚人的高速度進(jìn)行計算。然而，這種計算能力是有代價的;在學(xué)術(shù)界和工業(yè)界，核實一個現(xiàn)代的微處理器保證其操作的正確性越來越具有挑戰(zhàn)性。在微處理器應(yīng)用占據(jù)著核心地位的領(lǐng)域，如通信，醫(yī)藥，交通，財政，軍事等，對于處理器操作的可靠性和正確性要求更加的嚴(yán)格。為了給用戶提供更高的運算性能，新一代的處理器已可以將數(shù)百萬個晶體管集成在一起，這使得更復(fù)雜的設(shè)計變成可能；同時設(shè)計復(fù)雜度的增加使得驗證處理器的挑戰(zhàn)越來越大，因此影響到處理器的有效設(shè)計的整個過程。 在普遍的處理器設(shè)計周期中，初始階段的設(shè)計占據(jù)著最具決定性的地位，設(shè)計者都更加努力的去設(shè)想如何改進(jìn)設(shè)計中的傳統(tǒng)指標(biāo)，如性能，功耗和面積等。在這個期階段設(shè)計驗證未明確考慮。設(shè)計的驗證通常被認(rèn)為是設(shè)計完成后的任務(wù)，工程界的這一普遍的事實使的已經(jīng)完成的設(shè)計變得更加難以進(jìn)行驗證。因此為了及時消除關(guān)鍵的設(shè)計錯誤，處理器廠商被迫采用巨大的驗證團隊。目前，確保處理器設(shè)計正確性環(huán)節(jié)占創(chuàng)建這整個新的處理器設(shè)計過程的最大部分（高達(dá)70％），這就給計算行業(yè)消費分配帶來了重大挑戰(zhàn)。而在設(shè)計驗證過程中存在如此挑戰(zhàn)，主要的原因是在目前的處理器設(shè)計流程中存在的問題。 在這篇論文中，為了減少設(shè)計驗證所使用的時間，并提高驗證效率，我們建議，在設(shè)計周期的初始階段，考慮設(shè)計的可驗證性作為一個重要的設(shè)計約束。在上文中我們已經(jīng)表述了驗證環(huán)節(jié)在整個體系架構(gòu)設(shè)計中的重要性。我們已提供了在設(shè)計循環(huán)壽命中應(yīng)用基于斷言驗證的有效方法，驗證計劃作為驗證組的路線圖，我們的方法強調(diào)在驗證過程中寫作驗證計劃具有更好的優(yōu)勢。同時我們也描述了在設(shè)計周期末端添加斷言會給整個設(shè)計帶來更多的困難，整個設(shè)計開銷也會更大。若在設(shè)計的最后環(huán)節(jié)加入斷言驗證需要更長的時間，這對最終設(shè)計的完成是一個挑戰(zhàn)。 在本研究中，我們使用基于斷言的驗證（ABV）機制來驗證AMBER-25處理器的核心系統(tǒng)。在我們主要環(huán)節(jié)的驗證過程中使用了SystemVerilog斷言（SVA），通過我們的驗證過程已證明SVA在基于斷言的驗證中的有效性，SVA不僅可以捕捉系統(tǒng)設(shè)計的缺陷，而且可以提供斷言的驗證覆蓋率的詳細(xì)信息.我們提供了有效的，，并切可擴展的基于斷言的驗證模型。這種模式可以更容易的進(jìn)行功能驗證，并且保證了設(shè)計功能的正確性，而不會影響設(shè)計原來的性能，功耗和面積指標(biāo)。
【學(xué)位授予單位】：北京理工大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2014
【分類號】：TP332

【相似文獻(xiàn)】

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

1 Chun-Mei Zhang;Xiao-Tian Song;Patcharapong Treeviriyanupab;Mo Li;Chao Wang;Hong-Wei Li;Zhen-Qiang Yin;Wei Chen;Zheng-Fu Han;;Delayed error verification in quantum key distribution[J];Chinese Science Bulletin;2014年23期

2 杜振軍;馬光勝;馮剛;;A new model for verification[J];Journal of Harbin Institute of Technology;2007年03期

3 ;Symbolic algorithmic verification of intransitive generalized noninterference[J];Science China(Information Sciences);2012年07期

4 ;Random testing for system-level functional verification of system-on-chip[J];Journal of Systems Engineering and Electronics;2009年06期

5 ;Formal verification of safety protocol in train control system[J];Science China(Technological Sciences);2011年11期

6 ;Optimal design and verification of temporal and spatial filters using second-order cone programming approach[J];Science in China(Series F:Information Sciences);2006年02期

7 ;Optimization in Commercial UMTS Network[J];中國通信;2007年02期

8 Shihao Yan;Robert Malaney;;Location Verification Systems in Emerging Wireless Networks[J];ZTE Communications;2013年03期

9 Qian Junyan;Wu Juan;Zhao Lingzhong;Guo Yunchuan;;SUMMARIZATION OF BOOLEAN SATISFIABILITY VERIFICATION[J];Journal of Electronics(China);2014年03期

10 ;Formal verification technique for grid service chain model and its application[J];Science in China(Series F:Information Sciences);2007年01期

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

1 維克多（Nshunguyimfura Victor）;基于斷言的AMBER處理器驗證[D];北京理工大學(xué);2014年

本文編號：2187635