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

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

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

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