斷言（System Verilog Assertion 簡(jiǎn)稱SVA）可以被放在RTL設(shè)計(jì)或驗(yàn)證平臺(tái)中，方便在仿真時(shí)查看異常情況。一般在數(shù)字電路設(shè)計(jì)中都要加入斷言，斷言占整個(gè)設(shè)計(jì)的比例應(yīng)不少于30%。斷言通常被稱為序列監(jiān)視器或者序列檢驗(yàn)器，是對(duì)設(shè)計(jì)應(yīng)當(dāng)如何執(zhí)行特定行為的描述，是一種嵌入設(shè)計(jì)檢查。如果檢查的屬性（property）不是我們期望的表現(xiàn)，那么在我們期望事件序列出現(xiàn)異常情況，發(fā)生故障時(shí)，會(huì)產(chǎn)生警告或者錯(cuò)誤提示。
?
目錄
一、斷言的作用
二、斷言的種類
三、 并發(fā)斷言SVA組成
一、斷言的作用
1.檢查特定條件或事件序列的出現(xiàn)情況。
2.提供功能覆蓋
二、斷言的種類
1.立即斷言（Immediate?Assertions）
立即斷言具有非時(shí)序性特性，作為檢查當(dāng)前仿真時(shí)間的條件，執(zhí)行時(shí)如同過(guò)程語(yǔ)句相當(dāng)于 if else，需要放在過(guò)程塊中，如：initial、always、task、function。
語(yǔ)法：
? ? ? ? labels： assert（expression） action_block;
其中：
? ? ? ? (1)、action_block操作塊在斷言表達(dá)式expression之后立即執(zhí)行；
? ? ? ? (2)、action_block操作塊指定在斷言成功或失敗時(shí)采取什么操作；
? ? ? ? (3)、action_block類型：pass_statement；else fail_statement；
? ? ? ? (4)、labels為斷言名稱；
由于斷言表達(dá)式中所斷言的條件必須為真，因此斷言的失敗將具有與之相關(guān)的“嚴(yán)重”程度。默認(rèn)情況下，斷言失敗的嚴(yán)重程度是一個(gè)error。還可以結(jié)合$fatal/$error/$warning/$info給出不同嚴(yán)重級(jí)別的消息提示，嚴(yán)重等級(jí)依次遞減。
module alu(a,b,c,en)
input a,b;
input en;
output c;
reg a,b;
always @(posedge clk or negedge rst_n)
begin
if(!rst_n)
begin
c <= 0;
end
else if(a == b)
begin
check_a_and_b assert((a>=5) || (b>=5)) $display("expression evaluates value is true");
else
$error("expression evaluates value is false");
end
end
... ...
endmodule在a和b發(fā)生變化時(shí)，斷言語(yǔ)句被執(zhí)行。
2.并發(fā)斷言（Concurrent? Assertions）?
并發(fā)斷言具有時(shí)序性，通常使用關(guān)鍵詞property用來(lái)區(qū)分立即斷言和并發(fā)斷言。之所以稱之為并發(fā)，是由于斷言語(yǔ)句會(huì)與設(shè)計(jì)模塊一同并行執(zhí)行。我們可以認(rèn)為并發(fā)斷言是一個(gè)連續(xù)運(yùn)行的模塊，為整個(gè)仿真過(guò)程檢查信號(hào)，因此會(huì)在并發(fā)斷言內(nèi)設(shè)定一個(gè)采樣的時(shí)鐘。
? ? ? ? ?(1)、??并發(fā)斷言僅在有時(shí)鐘周期的情況下出現(xiàn)，基于時(shí)鐘周期執(zhí)行；
?????????(2)、? 測(cè)試表達(dá)式是基于所涉及變量的采樣值在時(shí)鐘邊緣進(jìn)行計(jì)算的；
?????????(3)、? 變量的采樣在預(yù)備階段完成，而表達(dá)式的計(jì)算在調(diào)度器的觀察階段完成；
? ? ? ? ?(4)、? 可以在過(guò)程塊、module、interface、program塊內(nèi)定義并發(fā)斷言；
? ? ? ? ?(5)、? 區(qū)分立即斷言和并發(fā)斷言的關(guān)鍵字是property。
語(yǔ)法：
? ? ? ? labels: assert property (判斷條件)
? ? ? ? 舉例：
a_b: assert property(@(posedge clk) not(a && b));其中：
? ? ? ? (1)、labels為斷言名稱；
? ? ? ? (2)、property（屬性）在每個(gè)時(shí)鐘的上升沿都被效驗(yàn)，不論a和b如何變化。
三、 并發(fā)斷言SVA組成
一條SVA并發(fā)斷言可以看成是由四種不同層次的結(jié)構(gòu)組成：
- 建立布爾表達(dá)式（booleans）
- 建立序列（sequence）
- 建立屬性（property）
- 建立斷言聲明（assertion statements）
1、布爾表達(dá)式
????????布爾表達(dá)式是構(gòu)成SVA的最基本單元。其一般形式為標(biāo)準(zhǔn)的SystemVerilog的布爾表達(dá)式，它由信號(hào)及其邏輯關(guān)系運(yùn)算符構(gòu)成，用以表示某個(gè)邏輯事件的發(fā)生。
2、序列
? ? ? ? 序列是布爾表達(dá)式在時(shí)間上的組合。在任何設(shè)計(jì)模型中，功能總是由多個(gè)邏輯事件的組合來(lái)表示。這些事件可以是簡(jiǎn)單的同一個(gè)時(shí)鐘邊緣被求值的布爾表達(dá)式，或者是經(jīng)過(guò)幾個(gè)時(shí)鐘周期的求值的事件。
? ? ? ? SVA中用序列(sequence)來(lái)表示這些事件，sequence可以讓斷言易讀，復(fù)用性高。具有以下特性：可以帶參數(shù)、可以在property中調(diào)用、可以使用局部變量、可以定義時(shí)鐘周期。
其基本語(yǔ)法是：
sequence Name_of_Sequence;
(test expression);
......
endsequence許多序列可以邏輯或者有序地組合起來(lái)生成更復(fù)雜的序列。
3、屬性
? ? ? ? SVA中用屬性(property)來(lái)表示這些復(fù)雜的有序行為。property是比seuence更高一層的單元，也是構(gòu)成斷言最常用的模塊。其中最重要的性質(zhì)是可以在property中使用蘊(yùn)含操作符（|-> |=>）。
其基本語(yǔ)法是：
property Name_of_Property;
(test expression); or
(complex sequence expressions)
endpropertyproperty就是SVA中需要用來(lái)判定的部分，用來(lái)模擬過(guò)程中被驗(yàn)證的單元，它必須在模擬過(guò)程中被斷言來(lái)發(fā)揮作用。
4、斷言
? ? ? ? SVA中用斷言（assert）來(lái)檢查這些屬性。其基本語(yǔ)法是：文章來(lái)源：http://www.zghlxwxcb.cn/news/detail-692310.html
assertion_name: assert property（property name）未完待續(xù)......文章來(lái)源地址http://www.zghlxwxcb.cn/news/detail-692310.html
到了這里，關(guān)于[SVA知識(shí)點(diǎn)一]: System verilog 斷言(assert)的基本介紹的文章就介紹完了。如果您還想了解更多內(nèi)容，請(qǐng)?jiān)谟疑辖撬阉鱐OY模板網(wǎng)以前的文章或繼續(xù)瀏覽下面的相關(guān)文章，希望大家以后多多支持TOY模板網(wǎng)！
