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

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

斷言驗證
斷言驗證就是在模擬中引入形式特征檢查的驗證方法。用這種方法，設計師編碼時插入對特征的描述——斷言。代碼完成后，進行模擬以檢查斷言，并修改模擬時斷言發現的問題。，特征檢查根據約束限定，窮舉搜索設計的狀態空間、證明或證偽斷言、查找設計的錯誤。斷言驗證，給模擬驗證的測試基準和監督技術帶來許多非常需要的技術手段，也有助于普及和接受正在出現的形式驗證技術。
使用斷言的核心想法是讓設計師把設計假設、意圖傳遞給驗證過程，改善了設計師和驗證師的溝通。設計師能利用驗證知識改善設計流程，而驗證師有了精確的設計特征來驗證。實際上，當設計師在設計過程中寫斷言時，進一步明確了假設和特征，因此寫出更好的代碼。另外，考慮到模塊的可驗證性，設計師更有可能選擇減少系統驗證成本的實現方式，從而得到了更易驗證和更高質量的設計。
設計師通過斷言形式捕獲規范、假設和設計的行為特征，以簡潔的格式捕獲設計意圖，從設計流程開始就剔除錯誤，同時使驗證過程自動化。用斷言捕獲接口約束，精確定義符合接口協議的可能行為。模擬時不斷檢查這些斷言，然后形式工具對斷言和RTL設計一起進行分析，搜索設計特征的反例。
驗證方法的核心是一個集成工具組，包括模擬、覆蓋率、約束驅動的測試生成和形式分析，該工具組為RTL設計的實現提供詳細驗證。斷言從使用角度把這些能力結合到一起。斷言用來監督模擬行為、驅動形式驗證、控制激勵生成，為全面的功能覆蓋率尺度打下基礎。

Property Specification Language (PSL)是一種專門用于硬件特性描述的語言，由IBM開發的Sugar語言發展而來。2002年Sugar語言被Accellera標準化組織選中作為工業標準加以發展形成PSL語言。PSL語言以其簡單易用且可應用于Verilog/VHDL/SystemC等多種設計語言的特性而被廣大設計公司和EDA公司采用。
同時PSL語言可在仿真代碼過程中直接被編譯成機器代碼而加以執行，減少了調用PLI任務時對仿真速度的影響，能有效地提高基于功能覆蓋率分析的仿真速度。
應用方案
下面我們就以AMBA AHB總線為例看一下如何使用PSL語言實現功能覆蓋率的分析。
圖2中顯示了AHB總線Four-beating wrapper burst命令的波形，以下列出的是我們用于檢測這一功能是否被執行的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功能是否在測試過程中被測試到，由此再增加相應的測試激勵或是改變隨機測試激勵的約束條件。通過分析AHB總線規范,將所有我們關心的功能使用PSL描述后，我們設計了基于PSL語言的功能覆蓋率IP，這個IP可以在以后的基于AMBA AHB總線的設計中重復使用。