硬件驗證語言(HVL)已經(jīng)度過了關(guān)鍵的早期采用者階段，現(xiàn)在正在積極進入主流。據(jù)估計，他們目前的滲透水平占整個Verilog和VHDL用戶市場的10%，年增長率超過50%。HVL市場目前由商業(yè)解決方案主導(dǎo)：Verisity Design Inc.的Specman Elite和Synopsys Inc.的Vera。其他商業(yè)解決方案包括Forte Design Systems的Rave和Co-Design Automation Inc.的新來者Superlog.開源解決方案，包括Cadence Design Systems Inc.的TestBuilder和Juniper Networks Inc.的Jeda。 C++ TCL或Perl，并通過自定義PLI接口與VHDL或Verilog集成。

　　如果您目前正在使用 Verilog 或 VHDL 來驗證您的設(shè)計，您是否應(yīng)該考慮在下一個項目中切換到驗證語言，或者您是否可以使用現(xiàn)有工具完成相同的任務(wù)?隨著80年代后期設(shè)計復(fù)雜性的增加，設(shè)計界被迫放棄其可靠的原理圖捕獲工具，擁抱邏輯綜合革命，以保持有競爭力的生產(chǎn)力水平。功能復(fù)雜性的持續(xù)增加迫使核查界對核查方式進行類似的改變。此更改涉及的不僅僅是使用自檢事務(wù)級測試平臺。盡管這種方法是成功使用 HVL 的必要步驟，但僅實現(xiàn)當(dāng)今一流的功能驗證方法還不夠。

　　HVL 的一個基本要求是支持高級數(shù)據(jù)類型、面向?qū)ο?、并發(fā)控制和設(shè)計可觀測性。通常正是這個基本要求促使用戶切換到C或C++來實現(xiàn)測試平臺，因為Verilog和VHDL都沒有提供所有這些功能。Verilog沒有高級數(shù)據(jù)類型，VHDL沒有設(shè)計的直接可見性。這兩種語言都不是面向?qū)ο蟮?，也沒有動態(tài)并發(fā)控制機制。C++與PLI接口相結(jié)合，可以輕松滿足這些要求。但這些基本要求只涉及編寫定向、自檢、事務(wù)級測試平臺的機制。它們沒有從根本上改變核查的實施方式。

　　為了在下一代數(shù)百萬門設(shè)計中具有競爭力，HVL必須提供三種互補工具，以實現(xiàn)新的、更高效的功能驗證方法：可約束的隨機生成、時間斷言和功能覆蓋。本文將討論這些工具。

　　隨著功能復(fù)雜性的增加，必須驗證的特征數(shù)量呈指數(shù)級增長。定向驗證方法，其中每個功能都使用單獨的手動編寫的測試用例單獨驗證，很快就會崩潰。需要編寫和調(diào)試的測試用例太多。在規(guī)定的上市時間窗口內(nèi)編寫所有這些測試用例所需的人數(shù)是難以管理的，而且成本太高 - 假設(shè)您設(shè)法找到它們。為了解決這個問題，約束隨機生成已被證明是一種有效的工具，可以有效地生成行使設(shè)計特征所需的激勵。

　　HVL 提供的可約束隨機生成比 Verilog 提供的簡單隨機數(shù)生成器和分發(fā)任務(wù)或 VHDL 中常用的隨機生成包強大得多。為了高效且高效地創(chuàng)建大量不同且有趣的場景，HVL 可以輕松生成有效復(fù)雜數(shù)據(jù)結(jié)構(gòu)的隨機實例。它們還可以輕松添加約束以將隨機生成定向到解決方案空間中特定有趣的區(qū)域，或者刪除約束以放寬某些條件以注入錯誤。圖 1 顯示了一個使用 OpenVera 語言編寫的編碼示例，該示例使用動態(tài)約束控制隨機生成 MAC 幀。

　　斷言語句

　　時態(tài)斷言是 HVL 的第二個要求。斷言是對屬性的陳述，該屬性必須始終為真。典型的軟件斷言是檢查指針的值是否為 NULL。使用 HDL 指定簡單斷言很容易。但是，在多個周期中具有多個替代方案的復(fù)雜、重疊的斷言更難表達、調(diào)試，更重要的是，更難信任。

　　HVL 包括一種強大的時態(tài)語言，可以使用簡潔的語法描述復(fù)雜的協(xié)議關(guān)系。動態(tài)生成并行執(zhí)行線程、檢測差異和報告錯誤的日常功能都是內(nèi)置的，使驗證工程師能夠?qū)Ｗ⒂谝炞C的實際功能，而不是檢測和報告機制。它們簡潔的語法和形式語義使它們非常適合通過形式驗證工具進行解釋，然后這些工具可能會嘗試在數(shù)學(xué)上證明或反駁該屬性。

　　盡管它們的力量很大，但時間斷言往往未被充分利用。這可能是由于它們的語法特征的聲明性和數(shù)學(xué)性質(zhì)挑戰(zhàn)了我們傳統(tǒng)的程序思維模式。這就是為什么大多數(shù)時態(tài)斷言示例(包括下面的示例)通常很簡單，并給人的印象是，時間斷言不值得為學(xué)習(xí)如何使用它們而進行投資。但是一旦理解，它們被證明是確保設(shè)計功能質(zhì)量不可或缺的工具。

　　在圖 2 中，使用 SuperLog 語言，斷言聲明請求后必須始終在 100 個時鐘周期內(nèi)進行授權(quán)或重試，除非應(yīng)用了重置，并且除非有請求，否則不得進行授權(quán)或重試。

　　HVL的最后一個基本要素是功能覆蓋。高級構(gòu)造將幫助您更輕松地對數(shù)據(jù)及其轉(zhuǎn)換進行建模。受約束的隨機生成將有助于自動創(chuàng)建測試用例，臨時斷言將有助于檢測功能錯誤。但是，您如何知道您已經(jīng)完全驗證了設(shè)計的功能呢?假設(shè)您的測試用例是隨機生成的，您如何知道是否已應(yīng)用所有相關(guān)測試用例?這就是功能覆蓋的用武之地。

　　補充保障

　　功能和代碼覆蓋率是互補的。后者測量代碼行，而前者測量數(shù)據(jù)模式、狀態(tài)序列及其與既定目標(biāo)的組合。代碼覆蓋率將檢測遺漏錯誤(“測試平臺是否忘記執(zhí)行這行代碼?”)，而功能覆蓋率檢測委托錯誤(“設(shè)計是否在所有可能的數(shù)據(jù)值序列下工作?”)。代碼覆蓋率可以幫助檢測現(xiàn)有代碼中的錯誤，但功能覆蓋率可以幫助查找未實現(xiàn)函數(shù)中的錯誤。

　　功能覆蓋率可以幫助回答以下問題：“我是否使用所有可能的尋址模式執(zhí)行了所有可能的操作數(shù)?“我是否向所有端口發(fā)送了所有重要長度的以太網(wǎng)數(shù)據(jù)包?”“我寫信給每個登記冊了嗎?”圖 3 顯示了一個編碼示例，該示例使用 Specman Elite 中的 e 語言來測量生成的 MAC 幀長度的功能覆蓋率。生成的報告的部分屏幕截圖使用戶能夠分析在設(shè)計驗證中還需要完成的工作。

　　本文 的 目的 是 說明 為什么 使用 專門 設(shè)計 用于 解決 功能 驗證 獨特 挑戰(zhàn) 的 語言 或 環(huán)境 比 以往 的 定向 測試 平臺 能 提供 更高 的 生產(chǎn)力 和 整體 質(zhì)量。這些挑戰(zhàn)通過易于約束的隨機生成、時間斷言和功能覆蓋來解決。但是，重要的是要注意，盡管這些功能體現(xiàn)在 HVL 中，但僅使用 HVL 并不一定意味著充分利用這些功能。必須區(qū)分學(xué)習(xí)語言和學(xué)習(xí)如何正確使用它。前者很容易。后者需要幾個月的經(jīng)驗或適當(dāng)?shù)母呒壏椒ㄅ嘤?xùn)。

　　—

　　Janick Bergeron，Qualis Design Corp.(俄勒岡州奧斯威戈湖)的首席技術(shù)官，是驗證協(xié)會(http://janick.bergeron.com/guild/)的主持人。他擁有超過 15 年的功能驗證經(jīng)驗，擁有滑鐵盧大學(xué)(安大略省滑鐵盧)的 MASc 學(xué)位和俄勒岡大學(xué)(尤金)的 MBA 學(xué)位。