基于斷言的驗證簡介 – 第 1 部分

基于斷言的驗證（ABV）是一種與傳統(tǒng)方法相比可以大大減少驗證過程的技術(shù).

ABV主要用于 ASIC 領(lǐng)域，但由于FPGA 設(shè)備的復(fù)雜性不斷增加，事實證明它在 FPGA 驗證流程中同樣至關(guān)重要。

然而，在我們開始慶祝芯片項目驗證周期大幅縮短的可能性之前，我們需要了解斷言以及如何將它們有效地集成到驗證方法中。

為了便于技術(shù)消化，斷言的介紹將分為兩部分。第一部分將解釋什么是斷言，討論語言并發(fā)展基本術(shù)語和思想。在第二部分中，我們將深入挖掘并介紹蘊涵的使用和“空洞真理”的概念以及斷言和覆蓋。

什么是斷言？

斷言最簡單的定義是“設(shè)備行為的抽象表示，在規(guī)范、驗證和實現(xiàn)中很有用……”

稍后我們會看到這個定義可以擴展為更準(zhǔn)確的描述，但現(xiàn)在就用這個定義了。

有兩種語言可用于表達(dá)斷言的實際應(yīng)用，即屬性規(guī)范語言（PSL）和SystemVerilog斷言子集（SVA） 。

PSL 可用于 VHDL、Verilog、 SystemVerilog和SystemC ，并且是 VHDL-2008 的子集。

SVA 是SystemVerilog語言的斷言相關(guān)子集，基于Superlog和OpenVera捐贈。它的斷言和屬性功能也借鑒了 PSL。

兩種語言都是 IEEE 標(biāo)準(zhǔn)。

哪種語言？

VHDL 設(shè)計人員可以同時使用 SVA 和 PSL，但通常選擇 PSL，因為它可以直接放入 VHDL 代碼中并有助于設(shè)計文檔，而 SVA 則不能。此外，PSL 現(xiàn)在是 VHDL 標(biāo)準(zhǔn) (2008) 的一部分，因此這意味著只需要使用一種語言。

Verilog 設(shè)計人員可以同時使用 PSL 和 SVA，但通常使用 SVA，因為當(dāng)直接放入 Verilog 代碼中時，它比 PSL 具有更多可用功能。此外， SystemVerilog和 Verilog 現(xiàn)在合并為一個標(biāo)準(zhǔn) - SystemVerilog 。

好消息是 PSL 和 SVA 屬性看起來幾乎相同。

為什么使用斷言？

斷言已經(jīng)成為 ASIC 設(shè)計中一種既定且流行的驗證方法，因此 FPGA設(shè)計可以從這一領(lǐng)域?qū)W習(xí)。重要的是，它們受 IEEE 標(biāo)準(zhǔn)（PSL、 SystemVerilog和 VHDL）管轄。

面向?qū)ο?a target="_blank">編程中處理類、對象、繼承等要容易得多。它們基于您作為設(shè)計師所熟悉的設(shè)計規(guī)范，因此更容易實施。

斷言在模擬中創(chuàng)建了額外的安全層，因為它們是對原始規(guī)范的引用，并且在進行綜合和實現(xiàn)迭代時非常有用。

斷言本質(zhì)上以它們的編寫方式創(chuàng)建“實時文檔”，這使得設(shè)計的管理變得更加容易。它們非常容易閱讀和解釋，這使得與設(shè)計團隊的共享變得更容易管理。

在哪里放置斷言？

所有工具都允許您將斷言放置在單獨的單元或文件中，并將它們“綁定”到常規(guī) RTL 代碼。驗證工程師喜歡這個想法，因為它允許文件獨立性，而 HDL 設(shè)計人員通常更喜歡將斷言直接放入代碼中以減少所需的文件量。

大多數(shù)模擬器允許您直接在 RTL 代碼中放置斷言。對于 PSL，這表示為注釋。對于SystemVerilog ，斷言可以直接放入代碼中。

例如： – psl屬性 p1 是... 或 // psl屬性 p2 是...

VHDL-2008 允許將 PSL 斷言直接放入代碼中（無需注釋）。

將斷言放入代碼中時需要小心，因為綜合工具通常不支持某些斷言，因此需要使用綜合編譯指示來管理它們。

發(fā)展基本術(shù)語和想法

術(shù)語“基于斷言的驗證”（ABV）通常用于描述整個驗證過程，但它不僅僅涉及斷言。

該流程由序列、屬性、斷言和覆蓋組成。

ABV的基本思想是“屬性”。屬性是對設(shè)計的特定行為的正式描述，例如“窗戶破裂觸發(fā)警報”或“安全在 30 秒內(nèi)響應(yīng)警報”。

驗證工具可以通過多種方式使用屬性，通過“斷言”屬性來驗證不會發(fā)生不好的事情，例如“斷言損壞的窗戶總是會觸發(fā)警報”。

或者，使用“覆蓋”來驗證是否發(fā)生了好事，例如“在 30 秒內(nèi)覆蓋了對觸發(fā)警報的響應(yīng)”。

深入挖掘這些屬性，如果你看一下典型的數(shù)字設(shè)計規(guī)范，它已經(jīng)充滿了用簡單的英語表達(dá)的設(shè)計屬性。作為設(shè)計人員，您可以將這些屬性重寫到 HDL 中，同時考慮到正確的硬件實現(xiàn)。

因此，屬性、斷言和覆蓋代表了設(shè)計的純粹行為（期望的或不期望的）。正如我們所說，它們可以作為非常有效的設(shè)計文檔，并作為設(shè)計驗證期間的參考。它們還被各種功能和形式驗證工具所接受。

我們現(xiàn)在需要了解如何定義屬性以及它如何使用“時間邏輯”的原理。

時態(tài)邏輯可以被認(rèn)為是添加了時間維度的布爾邏輯。

如果我們使用“離散時間”，則屬性表示設(shè)計的“狀態(tài)序列”。請注意，所有流行的基于屬性的設(shè)計 (PBD)/ABV 解決方案都對設(shè)計中對象的采樣值進行操作。

為了及時表達(dá)這種關(guān)系，屬性使用“時間”或“模態(tài)”運算符，例如下一個、最后、全局、直到（next, finally, globally, until）等。

接下來我們需要了解如何構(gòu)建屬性。

我們都熟悉的布爾類型表達(dá)式是屬性組成的一部分，但卻是最簡單的部分。我們還需要了解“序列” 。

“序列”通常被認(rèn)為是代表離散時間點上的一系列設(shè)計狀態(tài)的屬性的基本時間構(gòu)建塊。

典型的序列代表設(shè)計中的簡單執(zhí)行路徑。

要從簡單的序列創(chuàng)建真實的屬性，您可以：

“融合”序列，其中一個序列在另一個序列開始的同一時刻結(jié)束。

“連接”序列，其中一個序列結(jié)束，另一個序列在下一個時間點開始

說一個序列是另一個序列的“蘊含”

“與”或“或”序列

檢查一個序列是否包含在另一個序列中

檢查序列是否重復(fù)給定次數(shù)（連續(xù)或不連續(xù)）

一旦設(shè)計屬性正式化，所有工具都可以在兩個指令之一中使用這些屬性：

圖-1

斷言——當(dāng)屬性不成立時會發(fā)出警報。

覆蓋——確認(rèn)該屬性已成功測試。

一些工具（主要是形式驗證，但也有一些模擬器）允許更多指令，例如控制設(shè)計刺激或限制環(huán)境條件（假設(shè)、限制、公平等）。

建立實用的斷言

現(xiàn)在我們已經(jīng)了解了屬性和序列的基本元素，讓我們看看如何構(gòu)建實際的斷言。

正如我們所提到的，最基本的屬性是具有嚴(yán)格線性時間流的“序列”。

模擬需要線性時間流，因此屬性的時間來回跳躍是不可能的，因為這會使模擬變得不可能。

序列的每個節(jié)點代表您的設(shè)計的一種狀態(tài)：

某些信號所需的值

必須滿足的條件

為了完成序列，您必須指定如何將這些節(jié)點連接在一起。那么，讓我們看看一些“序列”屬性事實。

最簡單的序列是布爾表達(dá)式，但更常見的是，您會將多個表達(dá)式粘合在一起以形成“隨時間擴展”的復(fù)雜序列。

要使元素在同一時鐘上粘在一起，請在 PSL 中使用‘fusion’ (:) 或在 SVA 中使用“零時鐘延遲”(##0) ‘zero clock delay’ (##0)。

要在元素之間引入一個周期中斷，請在 PSL 中使用“串聯(lián)”(;) ‘concatenation’ (;)或在 SVA 中使用“一個周期延遲”(##1) ‘one cycle delay’ (##1)。

您可以使用 SVA 中的一系列值 (##[ m:n ]) 指定更長的延遲。

PSL 使用“連續(xù)重復(fù)運算符”（<序列>[ *m 到 n]）([*m to n])來指定“值范圍”延遲。如果沒有要重復(fù)的序列，則假定“True”是重復(fù)的參數(shù)。

現(xiàn)在我們已經(jīng)提到了重復(fù)，讓我們更正式地看看這個。

如果相同的條件應(yīng)保持超過一個周期，那么我們可以使用“連續(xù)重復(fù)運算符”，而不是使用串聯(lián)或一個周期延遲來重復(fù)條件。

該運算符在 PSL 和 SVA 中看起來相同：序列 [* Number_or_Range ] Sequence [* Number_or_Range].。

帶有數(shù)字的簡單形式表示序列應(yīng)該重復(fù)（保持）給定的次數(shù)： A[ *7]。

范圍版本表示序列應(yīng)在自然范圍內(nèi)保持任意數(shù)量的循環(huán)（要指定無限上限，請在 PSL 中使用“inf”或在 SVA 中使用“$”）： B[*1 to inf] B[*1:$]

讓我們用一個例子來說明：

圖3

在這里，我們看到了一個重復(fù)的例子，以及沒有重復(fù)的等效序列，并顯示了 PSL 和 SVA 的相同序列。

時鐘序列/復(fù)位和屬性

所有屬性語言都使用離散時間，這意味著必須指定時鐘或采樣方法。

如果未指定時鐘，則應(yīng)用最快的可用工具默認(rèn)值，在模擬器的情況下，這可能是周期等于模擬分辨率的時鐘。

如果大多數(shù)屬性都使用一種時鐘方法，則您可以指定“默認(rèn)時鐘”‘default clock’。

要指定時鐘事件，請在 PSL 中序列的末尾或 SVA 中的開頭使用“@<時鐘條件>”。

對于時鐘條件，請使用本機 HDL 中首選的時鐘檢測器，例如VHDL 中的“ rising_edge ”函數(shù)或Verilog 中的“ negedge ”。

我們還需要能夠處理重置，因為有時您可能正在進行屬性評估，并且發(fā)生重置，這會導(dǎo)致斷言失敗或其他不需要的情況。

幸運的是，PSL和SVA都提供了放棄屬性評估的機制，而不會產(chǎn)生不利影響。

PSL允許在屬性末尾添加“ async_abort ”或“ sync_abort ”運算符和重置條件。

always (({(A);(B)}) async_abort C=’1′) @rising_edge(CLK);

在屬性開頭添加“disable iff （條件）”短語。

@(posedge CLK) disable iff (C) A ##1 B;

總結(jié)一下時鐘和復(fù)位：

屬性中沒有默認(rèn)重置，但您可以擁有默認(rèn)時鐘（采樣事件）。

在 SVA 中將重置和時鐘應(yīng)用于屬性的文本順序是 PSL 中順序的鏡像。

圖4

綜上所述

我們引入了斷言，并發(fā)現(xiàn) PSL 和 SVA 屬性相似并且類似于設(shè)計要求。

我們開發(fā)了斷言的基本術(shù)語和思想，并討論了序列、屬性、斷言和覆蓋以及它們?nèi)绾涡纬稍O(shè)計屬性。我們還學(xué)習(xí)了如何定義屬性以及它如何遵循時序邏輯原則。最后，我們開始構(gòu)建一些實際的斷言來理解我們所介紹和討論的內(nèi)容。

如果您喜歡這個介紹，您可以期待第二部分，它將介紹蘊含在斷言中的使用及其在斷言中的重要性以及在模擬中的使用。

審核編輯 黃宇