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

【相似文獻】

相關期刊論文 前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期

相關碩士學位論文 前1條

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

本文編號：2187635