介紹

功能覆蓋、激勵(lì)生成和運(yùn)行管理是當(dāng)今功能驗(yàn)證的三大相互關(guān)聯(lián)的任務(wù)。其中，功能覆蓋率可以說(shuō)是最重要的，主要是因?yàn)楦采w率收斂是tape的主要標(biāo)準(zhǔn)。覆蓋率衡量標(biāo)準(zhǔn)提供了關(guān)鍵的反饋。如圖1所示，覆蓋率模型應(yīng)包括端到端功能覆蓋、主要接口的事務(wù)覆蓋、關(guān)鍵RTL結(jié)構(gòu)的結(jié)構(gòu)覆蓋和基本代碼覆蓋。

基于斷言的方法有助于發(fā)現(xiàn)bug，反饋回歸環(huán)境的質(zhì)量。這種方法不僅可以由驗(yàn)證實(shí)現(xiàn)，設(shè)計(jì)可以通過(guò)以斷言的形式描述他們對(duì)設(shè)計(jì)內(nèi)部操作的深入行為來(lái)提供check。

斷言和功能覆蓋實(shí)際上是同一枚硬幣的兩面。兩者都在寄存器傳輸水平（RTL）設(shè)計(jì)中提供詳細(xì)的觀察點(diǎn)。

指南

遵循指南可以使設(shè)計(jì)更容易。首先，將斷言放在RTL代碼中，以便它們可以與RTL代碼一起管理、更新和重復(fù)使用。接下來(lái)，通過(guò)適當(dāng)?shù)淖⑨寣嘌耘cRTL分開(kāi)；一些公司建議將ifdef/endif放在斷言周?chē)员銓⑺鼈兣懦趯?shí)現(xiàn)流程中的工具之外。

斷言不必復(fù)雜。事實(shí)上，根據(jù)我的經(jīng)驗(yàn)，簡(jiǎn)單的斷言通常和復(fù)雜的斷言一樣有用，包括捕捉復(fù)雜的bug。在接下來(lái)的部分中，我將探索如何將SystemVerilog 斷言屬性和覆蓋屬性置于在設(shè)計(jì)上。

首先，用于表示特殊信息的寄存器應(yīng)遵守預(yù)定義的合法值（gray_code、odd_parity、even_parity、one-hot）。例如，下面的寄存器聲明要求bus_state是one_hot編碼的，int_mask中的單個(gè)位是相互排斥的，hdl_cmd將只具有合法值。設(shè)計(jì)或者驗(yàn)證可以捕獲它們，以確保它們被功能驗(yàn)證所涵蓋。

接下來(lái)，當(dāng)寄存器用作計(jì)數(shù)器時(shí)，它們應(yīng)該相應(yīng)地存在概念（最小、最大、范圍、值、遞減、遞增、上溢出、下溢出等）。例如，在下面的寄存器聲明中，我們希望確保hdr_adr在1到26的范圍內(nèi)。對(duì)于bus_cnt，它不應(yīng)該下溢和溢出。對(duì)于計(jì)數(shù)器來(lái)說(shuō)，了解他們是否達(dá)到了高水位可能很有趣。驗(yàn)證團(tuán)隊(duì)可以進(jìn)行更多的覆蓋分析，但需要知道這些計(jì)數(shù)器的位置，這些指針通?？梢栽诟采w屬性中找到。

接下來(lái)，當(dāng)寄存器用作計(jì)數(shù)器時(shí)，它們應(yīng)該相應(yīng)地運(yùn)行（即與最小、最大、范圍、值、遞減、增量、增量、下流、溢出等的所有參數(shù)一致）。例如，在下面的寄存器聲明中，我們希望確保hdr_adr在1到26的范圍內(nèi)。對(duì)于bus_cnt，它不應(yīng)該下溢和上溢。對(duì)于計(jì)數(shù)器來(lái)說(shuō)，了解他們是否達(dá)到了高水位也可能很有趣。驗(yàn)證團(tuán)隊(duì)可以進(jìn)行更多的覆蓋率分析。

此外，重要的控制寄存器（狀態(tài)、地址和狀態(tài)）應(yīng)正確復(fù)位，并且不應(yīng)具有X或Z狀態(tài)。

在RTL開(kāi)發(fā)期間定期進(jìn)行檢查。例如，在下面的示例中，當(dāng)斷言cmd_write時(shí)，將發(fā)生DMA傳輸。然而，用戶沒(méi)有檢查cmd_ready。他假設(shè)當(dāng)cmd_write被采樣時(shí)，命令處理已經(jīng)準(zhǔn)備就緒。

下面的第一個(gè)斷言屬性有助于確保在斷言cmd_write時(shí)，信號(hào)cmd_ready為真。第二個(gè)斷言屬性確保xdma傳輸將在cmd_write之后發(fā)生。另一個(gè)覆蓋率屬性可以評(píng)估成功的DMA傳輸。

當(dāng)綜合指令與case語(yǔ)句一起使用時(shí)，確保假設(shè)對(duì)指定的case語(yǔ)句成立，并報(bào)告任何潛在的仿真/綜合不匹配。對(duì)于full_case指令，至少有一個(gè)case項(xiàng)為真，對(duì)于parall_case指令，最多有一個(gè)case項(xiàng)為真。例如，在下面的示例中，帶有“X”賦值的默認(rèn)分支用于幫助綜合優(yōu)化。永遠(yuǎn)不應(yīng)該達(dá)到它。可以添加斷言屬性來(lái)檢查此場(chǎng)景。然后，可以使用仿真和形式驗(yàn)證來(lái)驗(yàn)證它永遠(yuǎn)不會(huì)被執(zhí)行。與此同時(shí)，我們可以有一個(gè)覆蓋率屬性，可以獲取一些關(guān)鍵但罕見(jiàn)的條件。我們希望確保它們已經(jīng)通過(guò)仿真進(jìn)行了檢查和覆蓋。

有時(shí)候，只有一個(gè)分支變量應(yīng)該是真。例如，在下面的示例中，應(yīng)始終斷言其中一個(gè)信號(hào)（s0、s1或s2）。我們可以用one_hot屬性來(lái)驗(yàn)證這一點(diǎn)。同樣，覆蓋屬性可用于捕獲控制信號(hào)上的臨界值變化，例如當(dāng)pkg_type從`CTRL更改為3'b111時(shí)?？刂普Z(yǔ)句為定義這些覆蓋屬性提供了一個(gè)特別好的位置，因?yàn)樗锌刂菩盘?hào)和參數(shù)都在本地可用。

當(dāng)設(shè)計(jì)團(tuán)隊(duì)集成所有SoC模塊進(jìn)行芯片級(jí)仿真時(shí)，這些模塊通常無(wú)法相互通信。為了及早發(fā)現(xiàn)這些模塊間通信問(wèn)題，添加了協(xié)議監(jiān)視器來(lái)檢查片上總線和標(biāo)準(zhǔn)接口。在仿真過(guò)程中，協(xié)議監(jiān)視器確保模塊與其外部接口正確通信。通過(guò)收集統(tǒng)計(jì)數(shù)據(jù)和覆蓋信息，這些監(jiān)視器衡量驗(yàn)證環(huán)境的有效性。

隨著模塊的復(fù)雜性增加，內(nèi)部通信方案也越來(lái)越復(fù)雜。斷言對(duì)于驗(yàn)證這些模塊內(nèi)接口很有用。

覆蓋率和數(shù)據(jù)流統(tǒng)計(jì)對(duì)內(nèi)部接口和外部接口一樣重要。此類(lèi)信息證實(shí)了通過(guò)接口的數(shù)據(jù)流，并突出了任何潛在的“瓶頸”。

例如，在下面的數(shù)據(jù)傳輸波形中，我想確保數(shù)據(jù)有效信號(hào)斷言足夠長(zhǎng)的時(shí)間（兩到四個(gè)周期），并且當(dāng)斷言有效時(shí)數(shù)據(jù)總線是穩(wěn)定的。

接下來(lái)，在下面的握手?jǐn)?shù)據(jù)傳輸波形中，我想確保數(shù)據(jù)有效信號(hào)的斷言時(shí)間足夠長(zhǎng)，以便在斷言有效時(shí)數(shù)據(jù)總線是穩(wěn)定的，并且每個(gè)有效的斷言后都有一個(gè)ack。

計(jì)算資源、系統(tǒng)片上總線、互連、buffer和存儲(chǔ)器是邏輯結(jié)構(gòu)，通常由仲裁和復(fù)雜的控制邏輯共享和控制。在為設(shè)計(jì)創(chuàng)建驗(yàn)證環(huán)境時(shí)，團(tuán)隊(duì)傾向于首先關(guān)注整體規(guī)格。相反，它們不會(huì)強(qiáng)調(diào)這些資源控制邏輯的邊界情況。我看到許多回歸環(huán)境在這些關(guān)鍵場(chǎng)景提供的覆蓋率非常低。因此，有問(wèn)題的場(chǎng)景沒(méi)有被發(fā)現(xiàn)，包括重新流片成本高昂的故障。

在仲裁資源共享的控制器中，根據(jù)優(yōu)先級(jí)、權(quán)重或credit方案生成request和grant信號(hào)。我想確保仲裁方案正確，資源（總線、互連、內(nèi)存）一次只由一個(gè)master處理，并在再次分配之前取消分配。最好用參考模型方法檢查這種類(lèi)型的結(jié)構(gòu)?？梢岳肁ccellera OVL庫(kù)中的仲裁檢查器。預(yù)定義的仲裁包括優(yōu)先權(quán)、公平或輪訓(xùn)、FIFO和LRU。

ovl_arbiter檢查器可以在RTL代碼中實(shí)例化。它確保不應(yīng)在沒(méi)有請(qǐng)求的情況下發(fā)放grant，并且在一個(gè)周期內(nèi)只聲明一項(xiàng)grant，并在請(qǐng)求后[min_cks:max_cks]指定的時(shí)間窗口內(nèi)grant。除了檢查仲裁方案外，仲裁員checker還有一套全面的cover point和cover group，如cover_req_granted、cover_req_aborted、time_to_grant、concurrent_requests等。還可以添加額外的斷言屬性，以確保request和grant信號(hào)表現(xiàn)良好。例如，仲裁checker假設(shè)請(qǐng)求將保留，直到它被grant。我們可以為每個(gè)通道生成斷言屬性，如下所示。

總線橋、dma控制器和路由器等數(shù)據(jù)傳輸設(shè)備將數(shù)據(jù)包從一個(gè)接口傳輸?shù)搅硪粋€(gè)接口。在系統(tǒng)級(jí)仿真環(huán)境中，數(shù)據(jù)完整性錯(cuò)誤不容易觀察到。只有當(dāng)損壞的數(shù)據(jù)到達(dá)scoreboard時(shí)，它們才會(huì)被檢測(cè)到，或者在仿真結(jié)束時(shí)被標(biāo)記為丟失。使用斷言屬性，可以沿著數(shù)據(jù)傳輸路徑檢查它們。它們不應(yīng)該丟失或損壞，如有必要，我們還可以確保它們遵循先入先出規(guī)格，沒(méi)有任何更改。與其手動(dòng)創(chuàng)建數(shù)據(jù)完整性斷言，不如利用Accellera OVL庫(kù)中的fifo斷言檢查器。fifo檢查器確保模塊中事務(wù)通過(guò)模塊的數(shù)據(jù)傳輸不會(huì)損壞。對(duì)于具有多個(gè)輸入和輸出端口的模塊，例如N-to-M總線矩陣，可以使用OVL多端口fifo檢查器。同樣，fifo檢查器還有一套全面的cover point和cover group，如cover_enqueues、cover_dequeues、cover_fifo_full、cover_fifo_empty、cover_simultaneous_enq_deq等。它們可用于評(píng)估設(shè)備的數(shù)據(jù)流。也可以添加其他斷言屬性。

出于驗(yàn)證目的，我們將有限狀態(tài)機(jī)（FSM）分為兩類(lèi)：接口FSM和計(jì)算FSM。接口FSM使用具有明確timing要求的I/O信號(hào)。接口FSM的例子有總線控制器、握手FSM等。計(jì)算FSM不涉及具有明確定義的timing要求的信號(hào)。重要的是不要根據(jù)FSM的RTL編寫(xiě)屬性。如果設(shè)計(jì)師誤解了需求或在編寫(xiě)RTL時(shí)犯了錯(cuò)誤，F(xiàn)SM將是錯(cuò)誤的。

通常，接口FSM的規(guī)范來(lái)自協(xié)議文檔和波形圖。斷言屬性應(yīng)來(lái)自原始規(guī)范。他們將確保FSM在時(shí)間段內(nèi)正確采樣輸入信號(hào)，并在輸出時(shí)序規(guī)范內(nèi)斷言響應(yīng)信號(hào)。通常，計(jì)算FSM的規(guī)范來(lái)自控制流圖，這在工程文檔和標(biāo)準(zhǔn)規(guī)范中很常見(jiàn)。為了提高性能和/或簡(jiǎn)化實(shí)現(xiàn)，流程圖可能會(huì)被劃分、扁平化、重新管道化成多個(gè)FSM。我們可以捕獲具有斷言屬性的流程圖行為創(chuàng)建了一個(gè)“可執(zhí)行”規(guī)范。

斷言屬性可用于捕獲流程圖中的控制決策、狀態(tài)跳變和操作序列。在下面的示例中，流程圖來(lái)自原始規(guī)范。

結(jié)論

在覆蓋率驅(qū)動(dòng)的驗(yàn)證方法中，捕獲錯(cuò)誤和衡量進(jìn)度的能力同樣重要。幸運(yùn)的是可以利用用斷言捕獲錯(cuò)誤以及在設(shè)計(jì)中提供深入的結(jié)構(gòu)覆蓋。通過(guò)使用覆蓋屬性和斷言庫(kù)，你可以以很少的增量努力完成這項(xiàng)工作。

最好的建議：在為設(shè)計(jì)開(kāi)發(fā)斷言時(shí)考慮覆蓋范圍。這是在回歸環(huán)境中實(shí)現(xiàn)全面的錯(cuò)誤檢測(cè)能力和結(jié)構(gòu)覆蓋率的第一步。

審核編輯：劉清