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

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

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

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

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

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

　　斷言語(yǔ)句

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

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

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

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

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

　　補(bǔ)充保障

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

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

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

　　—

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