設(shè)計復(fù)雜度的增加、IP重用等當(dāng)前復(fù)雜SoC/ASIC設(shè)計的特性要求對設(shè)計的功能進(jìn)行更加充分的驗證?；赑SL的功能覆蓋率分析與傳統(tǒng)的代碼覆蓋率分析共同構(gòu)成了一個完整的衡量電路驗證質(zhì)量的尺度，這一全新設(shè)計方法學(xué)的使用將有效 提高驗證的質(zhì)量和效率。
　　隨著集成電路的廣泛應(yīng)用，對功能正確性及速度、功耗、可靠性等都有嚴(yán)格要求。其中，功能正確性是基本的要求。2003 年度的國際半導(dǎo)體技術(shù)發(fā)展（International Technology Roadmap for Semiconductor, ITRS2003）指出，驗證已經(jīng)成為集成電路設(shè)計流程中開銷的工作。在目前的工程項目中，驗證工程師的數(shù)目超過了設(shè)計工程師，對于復(fù)雜的設(shè)計更是達(dá)到了2:1 或者3:1 的比率。造成這種局面的原因有二 ：一方面，設(shè)計的規(guī)模正如摩爾定律所指出的呈指數(shù)增長。如果用設(shè)計中的狀態(tài)數(shù)目來衡量功能復(fù)雜度的話，則設(shè)計的功能復(fù)雜度隨著設(shè)計規(guī)模又呈指數(shù)增長。如此驚人的速度，對驗證技術(shù)的處理能力提出了極大挑戰(zhàn)。另一方面，歷史上對設(shè)計流程中的其它環(huán)節(jié)（如邏輯綜合、布局布線、測試產(chǎn)生等問題）關(guān)注頗多，而對驗證重視不夠，造成驗證成為目前的瓶頸。如果沒有重大突破的話，驗證將成為未來集成電路設(shè)計工業(yè)流程中的重大障礙。

　　功能覆蓋率
　　隨著集成電路設(shè)計規(guī)模越來越大，使得窮盡模擬所有的輸入組合的方式在計算上逐漸不可行。如何利用合理的時間和計算資源達(dá)到理想的模擬效果，這是一個具有實際意義的問題。同時隨著隨機激勵生成技術(shù)的發(fā)展，約束（coNStrains）和偏置（biasing）技術(shù)大大提高了隨機向量的質(zhì)量，與傳統(tǒng)的隨機驗證相比，約束化的隨機指令生成可以在更短時間內(nèi)執(zhí)行更大量的相關(guān)測試，并且達(dá)到高覆蓋率。隨機激勵生成實現(xiàn)了自動化，但是基本上沒有考慮檢測設(shè)計錯誤的能力，因此如何確定約束化的隨機驗證效果也是一個不容忽視的問題。解決這兩個問題通常的做法就是運用覆蓋評估技術(shù)。在模擬驗證中，覆蓋評估能夠量化地度量模擬激勵集的完備性。同時，對于當(dāng)前的激勵集來說，覆蓋評估技術(shù)能夠診斷出哪部分設(shè)計尚未充分驗證，有助于后續(xù)的激勵生成。
　　覆蓋評估技術(shù)起源于軟件測試。其中的覆蓋評估主要以代碼為對象，如：語句、分支、表達(dá)式、路徑等等。由于用硬件描述語言所寫的設(shè)計也是一種軟件，所以代碼覆蓋評估很容易從軟件測試領(lǐng)域移植到設(shè)計驗證中來。這種評估技術(shù)簡單易行，但是其評估能力較弱。由此出發(fā)，結(jié)合硬件設(shè)計的特點，派生了其它的覆蓋評估技術(shù)，例如電路結(jié)構(gòu)覆蓋、有限狀態(tài)機覆蓋等等。
　　現(xiàn)有的商用HDL代碼覆蓋率工具通過在HDL代碼中插入特殊的PLI(Programming Language Interface)任務(wù)在動態(tài)仿真過程中捕獲代碼覆蓋率。圖1中顯示了商用代碼覆蓋率工具的使用方法。由于仿真過程中調(diào)用大量PLI任務(wù)造成仿真速度的降低，因此隨著設(shè)計規(guī)模的增大，代碼覆蓋率分析的效率也越來越低。
　　功能覆蓋率主要是面對設(shè)計的功能而不是HDL(Hardware Description Language)代碼，所以使用斷言語句驗證功能覆蓋率可以更有效地描述所需捕獲的邊腳邏輯以及所有感興趣的數(shù)據(jù)及控制信號的組合。這里描述的功能覆蓋率可以被認(rèn)為是斷言規(guī)范的一種延伸，從某種意義上用戶不再需要為了測試功能覆蓋率而再描述那些復(fù)雜的表達(dá)式。那些用于描述設(shè)計功能、變量以及其他行為的斷言語句都可以用來作為功能覆蓋率的建立基礎(chǔ)。通過觀察每一條斷言語句如何被執(zhí)行，用戶可以了解驗證是否達(dá)到了所需要的覆蓋率。
　　代碼覆蓋率與功能覆蓋率的關(guān)鍵不同點在于：在驗證過程中，代碼覆蓋率檢測激勵所執(zhí)行測試代碼的驗證效率；而功能覆蓋率用于檢測激勵所執(zhí)行代碼功能的效率。傳統(tǒng)上，設(shè)計功能的驗證是基于動態(tài)的仿真，通過觀察仿真結(jié)果發(fā)現(xiàn)、定位設(shè)計的缺陷。隨著ASIC和SoC設(shè)計復(fù)雜性的增加，如何有效地構(gòu)建設(shè)計的測試激勵，縮短驗證周期，這些為功能驗證帶來了巨大的挑戰(zhàn)。因此高效率的測試激勵自動生成技術(shù)也是當(dāng)前設(shè)計驗證的熱點技術(shù)之一。測試激勵自動生成的是帶約束的隨機測試激勵自動生成。由于隨機測試激勵技術(shù)的產(chǎn)生，簡單的100％的代碼覆蓋率已無法保證設(shè)計被100％的驗證。而功能測試覆蓋率可以更有效地告訴哪些功能已經(jīng)經(jīng)過測試，根據(jù)這些信息我們可以動態(tài)調(diào)整產(chǎn)生隨機測試激勵的約束條件，從而明顯地提高測試效率。但是，功能覆蓋率還不能完全替代代碼覆蓋率的所有工作，代碼覆蓋率在保證代碼書寫質(zhì)量上仍有著重要的地位，只有當(dāng)代碼覆蓋率和功能覆蓋率都達(dá)到100％時，我們才可以認(rèn)為我們的設(shè)計得到了比較好的驗證（即使代碼覆蓋率和功能覆蓋率都達(dá)到100％，也不代表設(shè)計已被100％完全驗證）。功能覆蓋率與代碼覆蓋率結(jié)合在一起，可以為設(shè)計和驗證提供一個完整的質(zhì)量驗證標(biāo)尺。

　　斷言驗證 斷言驗證就是在模擬中引入形式特征檢查的驗證方法。用這種方法，設(shè)計師編碼時插入對特征的描述——斷言。代碼完成后，進(jìn)行模擬以檢查斷言，并修改模擬時斷言發(fā)現(xiàn)的問題。，特征檢查根據(jù)約束限定，窮舉搜索設(shè)計的狀態(tài)空間、證明或證偽斷言、查找設(shè)計的錯誤。斷言驗證，給模擬驗證的測試基準(zhǔn)和監(jiān)督技術(shù)帶來許多非常需要的技術(shù)手段，也有助于普及和接受正在出現(xiàn)的形式驗證技術(shù)。
　　使用斷言的想法是讓設(shè)計師把設(shè)計假設(shè)、意圖傳遞給驗證過程，改善了設(shè)計師和驗證師的溝通。設(shè)計師能利用驗證知識改善設(shè)計流程，而驗證師有了的設(shè)計特征來驗證。實際上，當(dāng)設(shè)計師在設(shè)計過程中寫斷言時，進(jìn)一步明確了假設(shè)和特征，因此寫出更好的代碼。另外，考慮到模塊的可驗證性，設(shè)計師更有可能選擇減少系統(tǒng)驗證成本的實現(xiàn)方式，從而得到了更易驗證和更高質(zhì)量的設(shè)計。
　　設(shè)計師通過斷言形式捕獲規(guī)范、假設(shè)和設(shè)計的行為特征，以簡潔的格式捕獲設(shè)計意圖，從設(shè)計流程開始就剔除錯誤，同時使驗證過程自動化。用斷言捕獲接口約束，定義符合接口協(xié)議的可能行為。模擬時不斷檢查這些斷言，然后形式工具對斷言和RTL設(shè)計一起進(jìn)行分析，搜索設(shè)計特征的反例。
　　驗證方法的是

一個集成工具組，包括模擬、覆蓋率、約束驅(qū)動的測試生成和形式分析，該工具組為RTL設(shè)計的實現(xiàn)提供詳細(xì)驗證。斷言從使用角度把這些能力結(jié)合到一起。斷言用來監(jiān)督模擬行為、驅(qū)動形式驗證、控制激勵生成，為全面的功能覆蓋率尺度打下基礎(chǔ)。
　　Property Specification Language (PSL)是一種專門用于硬件特性描述的語言，由IBM開發(fā)的Sugar語言發(fā)展而來。2002年Sugar語言被Accellera標(biāo)準(zhǔn)化組織選中作為工業(yè)標(biāo)準(zhǔn)加以發(fā)展形成PSL語言。PSL語言以其簡單易用且可應(yīng)用于Verilog/VHDL/SystemC等多種設(shè)計語言的特性而被廣大設(shè)計公司和EDA公司采用。
　　同時PSL語言可在仿真代碼過程中直接被編譯成機器代碼而加以執(zhí)行，減少了調(diào)用PLI任務(wù)時對仿真速度的影響，能有效地提高基于功能覆蓋率分析的仿真速度。

　　應(yīng)用方案
　　下面我們就以AMBA AHB總線為例看一下如何使用PSL語言實現(xiàn)功能覆蓋率的分析。
　　圖2中顯示了AHB總線Four-beating wrapper burst命令的波形，以下列出的是我們用于檢測這一功能是否被執(zhí)行的PSL代碼。
　　/ psl sequence StartTransfer = {(HTrans == NONSEQ)};
　　/ psl sequence MidTransfer = {
　　/ ((HTrans == BUSY) || (HTrans == SEQ)) };
　　/ psl sequence EndTransfer = {
　　/ ((HTrans == NONSEQ) || (HTrans == IDLE))};
　　/ psl cover_Wrap4WriteBurst: cover {
　　/ {(HBurst== WRAP4) && (HWrite == 1'b1)} :
　　/ {{StartTransfer}; {MidTransfer[+]};{EndTransfer}} };
　　通過這些代碼我們可以分析Four-beating wrapper burst功能是否在測試過程中被測試到，由此再增加相應(yīng)的測試激勵或是改變隨機測試激勵的約束條件。通過分析AHB總線規(guī)范,將所有我們關(guān)心的功能使用PSL描述后，我們設(shè)計了基于PSL語言的功能覆蓋率IP，這個IP可以在以后的基于AMBA AHB總線的設(shè)計中重復(fù)使用。