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

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

ABV主要用于 ASIC 領域，但由于FPGA 設備的復雜性不斷增加，事實證明它在 FPGA 驗證流程中同樣至關重要。

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

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

什么是斷言？

斷言最簡單的定義是“設備行為的抽象表示，在規范、驗證和實現中很有用……”

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

有兩種語言可用于表達斷言的實際應用，即屬性規范語言（PSL）和SystemVerilog斷言子集（SVA） 。

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

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

兩種語言都是 IEEE 標準。

哪種語言？

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

Verilog 設計人員可以同時使用 PSL 和 SVA，但通常使用 SVA，因為當直接放入 Verilog 代碼中時，它比 PSL 具有更多可用功能。此外， SystemVerilog和 Verilog 現在合并為一個標準 - SystemVerilog 。

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

為什么使用斷言？

斷言已經成為 ASIC 設計中一種既定且流行的驗證方法，因此 FPGA設計可以從這一領域學習。重要的是，它們受 IEEE 標準（PSL、 SystemVerilog和 VHDL）管轄。

面向對象編程中處理類、對象、繼承等要容易得多。它們基于您作為設計師所熟悉的設計規范，因此更容易實施。

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

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

在哪里放置斷言？

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

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

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

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

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

發展基本術語和想法

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

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

ABV的基本思想是“屬性”。屬性是對設計的特定行為的正式描述，例如“窗戶破裂觸發警報”或“安全在 30 秒內響應警報”。

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

或者，使用“覆蓋”來驗證是否發生了好事，例如“在 30 秒內覆蓋了對觸發警報的響應”。

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

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

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

時態邏輯可以被認為是添加了時間維度的布爾邏輯。

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

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

接下來我們需要了解如何構建屬性。

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

“序列”通常被認為是代表離散時間點上的一系列設計狀態的屬性的基本時間構建塊。

典型的序列代表設計中的簡單執行路徑。

要從簡單的序列創建真實的屬性，您可以：

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

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

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

“與”或“或”序列

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

檢查序列是否重復給定次數（連續或不連續）

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

圖-1

斷言——當屬性不成立時會發出警報。

覆蓋——確認該屬性已成功測試。

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

建立實用的斷言

現在我們已經了解了屬性和序列的基本元素，讓我們看看如何構建實際的斷言。

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

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

序列的每個節點代表您的設計的一種狀態：

某些信號所需的值

必須滿足的條件

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

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

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

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

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

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

現在我們已經提到了重復，讓我們更正式地看看這個。

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

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

帶有數字的簡單形式表示序列應該重復（保持）給定的次數： A[ *7]。

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

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

圖3

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

時鐘序列/復位和屬性

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

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

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

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

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

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

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

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;

總結一下時鐘和復位：

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

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

圖4

綜上所述

我們引入了斷言，并發現 PSL 和 SVA 屬性相似并且類似于設計要求。

我們開發了斷言的基本術語和思想，并討論了序列、屬性、斷言和覆蓋以及它們如何形成設計屬性。我們還學習了如何定義屬性以及它如何遵循時序邏輯原則。最后，我們開始構建一些實際的斷言來理解我們所介紹和討論的內容。

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

審核編輯 黃宇