硬件驗(yàn)證語言(HVL)已經(jīng)度過了關(guān)鍵的早期采用者階段，現(xiàn)在正在積極進(jìn)入主流。據(jù)估計(jì)，他們目前的滲透水平占整個(gè)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 來驗(yàn)證您的設(shè)計(jì)，您是否應(yīng)該考慮在下一個(gè)項(xiàng)目中切換到驗(yàn)證語言，或者您是否可以使用現(xiàn)有工具完成相同的任務(wù)?隨著80年代后期設(shè)計(jì)復(fù)雜性的增加，設(shè)計(jì)界被迫放棄其可靠的原理圖捕獲工具，擁抱邏輯綜合革命，以保持有競爭力的生產(chǎn)力水平。功能復(fù)雜性的持續(xù)增加迫使核查界對核查方式進(jìn)行類似的改變。此更改涉及的不僅僅是使用自檢事務(wù)級測試平臺。盡管這種方法是成功使用 HVL 的必要步驟，但僅實(shí)現(xiàn)當(dāng)今一流的功能驗(yàn)證方法還不夠。

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

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

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

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

　　斷言語句

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

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

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

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

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

　　補(bǔ)充保障

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

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

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

　　—

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