01 何為斷言

斷言主要用來(lái)檢查仿真過(guò)程中存在的時(shí)序問(wèn)題，如果存在異常情況，斷言會(huì)報(bào)警。一般在數(shù)字電路設(shè)計(jì)中都要加入斷言，斷言占整個(gè)設(shè)計(jì)的比例應(yīng)不少于30%。

02 斷言的作用

· 使用斷言可以縮短研制周期；

· 使用斷言可以使設(shè)計(jì)中存在的各種問(wèn)題更容易被動(dòng)態(tài)監(jiān)測(cè)觀察；

· 使用斷言內(nèi)嵌的覆蓋率統(tǒng)計(jì)功能（cover）可以更加容易的獲得對(duì)于功能的覆蓋性；

· 斷言的可讀性較一般描述語(yǔ)言更容易理解；

· 通過(guò)全局控制實(shí)現(xiàn)設(shè)計(jì)中斷言的開(kāi)關(guān)；

· 斷言可以加速形式驗(yàn)證，提高形式驗(yàn)證的效率；

03 斷言的種類(lèi)

斷言分為立即斷言和并行斷言

3.1 立即斷言

立即斷言主要用來(lái)檢查當(dāng)前仿真時(shí)間的條件，可以理解為if...else，放在過(guò)程塊中使用。

語(yǔ)法：

labels：assert（expression）action_block;

· action_block 操作塊在斷言表達(dá)式的求值之后立即執(zhí)行；

· 操作塊指定在斷言成功或失敗時(shí)采取什么操作；

· action_block: pass_statement; else fail_statement;

例子：

assert(expression) $display("expression evaluates to true");

else $fatal("expression evaluates to false");

斷言失敗默認(rèn)嚴(yán)重程度為error，error達(dá)到一定數(shù)量仿真會(huì)退出

立即斷言構(gòu)建思路：

3.2 并發(fā)斷言

并發(fā)斷言檢 查跨越多個(gè)時(shí)鐘周期的事件序列 。

可以認(rèn)為并發(fā)斷言是一個(gè)連續(xù)運(yùn)行的模塊，為整個(gè)仿真過(guò)程檢查信號(hào)，所以需要在并發(fā)斷言內(nèi)指定一個(gè)采樣時(shí)鐘。

· 并發(fā)斷言僅在有時(shí)鐘周期的情況下出現(xiàn)

· 測(cè)試表達(dá)式是基于所涉及變量的采樣值在時(shí)鐘邊緣進(jìn)行計(jì)算的

· 可以在過(guò)程塊、module、interface和program塊內(nèi)定義并發(fā)斷言

· 區(qū)別并發(fā)斷言和立即斷言的關(guān)鍵字是property

格式：

斷言名：assert property (判斷條件)

例子：

check_a_and_b:assert property (@(posedge clk) (a&&b))

$display("a&&b is true");

else

$error ("a&&b is false")；

04 斷言層次結(jié)構(gòu)

SVA中可以存在內(nèi)建的單元，這些單元可以是以下的幾種：

Boolean expressions 布爾表達(dá)式

布爾表達(dá)式是組成斷言的最小單元，斷言可以由多個(gè)邏輯事件組成，這些邏輯事件可以是簡(jiǎn)單的布爾表達(dá)式.在SVA中，信號(hào)或事件可以使用常用的操作符，如：&&, ||, !, ^，& 等；

Sequence序列

sequence是布爾表達(dá)式更高一層的單元，一個(gè)sequence中可以包含若干個(gè)布爾表達(dá)式，同時(shí)在sequence中可以使用一些新的操作符，如 ## 、重復(fù)操作符、序列操作符

Property 屬性

property是比sequence更高一層的單元，也是構(gòu)成斷言最常用的模塊，其中最重要的性質(zhì)是可以在property中使用蘊(yùn)含操作符(|-> |=>)；

4.1 sequence 序列

在任何設(shè)計(jì)中，功能總是由多個(gè)邏輯事件的組合來(lái)表示，這些事件可以是簡(jiǎn)單的同一個(gè)時(shí)鐘沿被求值的布爾表達(dá)式，也可以是經(jīng)過(guò)幾個(gè)時(shí)鐘周期的求值事件，SVA用關(guān)鍵字sequence來(lái)表示這些事件，sequence可以讓斷言易讀，復(fù)用性高。

sequence具有如下特性：

? 可帶參數(shù)；

? 可以在 property 中調(diào)用；

? 可以使用局部變量；

? 可以定義時(shí)鐘周期；

sequence的定義格式如下：

sequence name_of_sequence(參數(shù));

……

endsequence

以下代碼分別通過(guò)property，sequence+property實(shí)現(xiàn)對(duì)a&&b仿真時(shí)間的判斷：

//1.使用property實(shí)現(xiàn)對(duì)a&&b時(shí)序的判斷
check_a_and_b:assert property(@(posedge clk) (a&&b)) 
    $display("a&&b is true");
else     
$error("a&&bisfalse");


//2.使用sequence+property實(shí)現(xiàn)對(duì)a&&b時(shí)序的判斷


sequence seq_a_and_b;
    @(posedge clk) a&&b;
endsequence


//在斷言的property中調(diào)用sequence
check_a_and_b: assert property(seq_a_and_b) 
    $display("a&&b is true");
else 
    $error("a&&b is false");

sequence 序列可以帶參數(shù)：

格式：

sequence seq1(signal1,signal2);

@(posedge clk) signal1&&signal2;

endsequence

用法：

sequence seq1(signal1,signal2);
    @(posedge clk) signal1&&signal2;
endsequence
//在斷言的property中調(diào)用sequence
check_a_and_b: assert property(seq1(a,b)) 
    $display("a&&b is true");
else 
    $error("a&&b is false");

帶時(shí)序關(guān)系的sequence ：在SVA中時(shí)鐘延時(shí)用符號(hào)"##"來(lái)表示，如"##2"表示延時(shí)兩個(gè)時(shí)鐘周期；

例如：

sequence seq2;
    @(posedge clk) a ##2 b ;
endsequence


//在斷言的property中調(diào)用sequence
check_a_and_b: assert property(seq2);

sequence會(huì) 在時(shí)鐘上升沿到來(lái)后首先檢查 a 是否為 1，當(dāng)a為1時(shí)，兩個(gè)時(shí)鐘周期后繼續(xù)檢查b是否為1，當(dāng)b為1時(shí)，斷言pass ；

sequence 序列可以內(nèi)嵌

格式：

sequence seq1;

@(posedge clk) a&&b;

endsequence

sequence seq2;

seq1;

endsequence

4.2 property 序列

property是比sequence更高一層的單元，也是構(gòu)成斷言最常用的模塊，其中最重要的性質(zhì)是可以在

property中使用 蘊(yùn)含(overlapped)操作符(|-> |=>).

格式：

property的定義格式如下：

property name_of_property(參數(shù)列表);

測(cè)試表達(dá)式或復(fù)雜的sequence；

endproperty

property就是SVA中需要用來(lái)判定的部分，用來(lái)模擬過(guò)程中被驗(yàn)證的單元，它必須在模擬過(guò)程中被斷言來(lái) 發(fā)揮作用，SVA提供了關(guān)鍵字 assert 來(lái)檢查屬性，assert的基本語(yǔ)法是：

assertion_name: assert property(property_name)

else

$display("SVA error");

并行斷言構(gòu)建思路：

05 sequence和property的異同

· 任何在sequence中的表達(dá)式都可以放到property中；

· 任何在property中的表達(dá)式也可以搬到sequence中，但是只有在property中才能使用蘊(yùn)含操作符；

· property中可以例化其他property和sequence，sequence中也可以調(diào)用其他sequence，但是不能例化property；

· property需要用cover /assert/assume 等關(guān)鍵字進(jìn)行實(shí)例化，而sequence直接調(diào)用即可。

除了以上的區(qū)別外，立即斷言和并發(fā)斷言的采樣時(shí)間是否相同也是驗(yàn)證過(guò)程中需要注意的問(wèn)題，以下的代碼進(jìn)行演示：

//SVA
module inline(
input       clk,
input        a,
input        b,
input [7:0]  d1,
input [7:0]  d2,
output[7:0]  d3,
output[7:0]  d4
);


reg [7:0] d3=8'h0;
reg[7:0]d=48'h0;


always@(posedge clk) begin
if(a) begin
d3<=d1;
end
if(b) begin
d4<=d2;
end
end
endmodule


module top;
reg       clk;
reg         a;
reg          b;
reg [7:0]    d1;
reg [7:0]    d2;
wire [7:0]  d3;
wire [7:0]  d4;
initial?begin


$fsdbDumpfile("wave/top.fsdb");
$fsdbDumpvars();
$fsdbDumpSVA();
end


initial begin
#0 clk=0;
forever begin 
#5 clk=~clk;
    end
end


always begin
a<=$random()%2;
b<=$random()%2;
d1<=$random()%256;
d2<=$random()%256;
end
// immesiate assertions
always@(posedge clk) begin
check_a_and_b:assert(a&&b) $display("a&&b is turn");
else $error("a&&b is false");
end
// concurrent assertions
property p_mutex;
@(posedge clk) not(a&&b);
endproperty
a_mutex: assert property(p_mutex)$display("a&&b is success");
else $error("a&&b is fail");
initial begin
#300;
     $finish;
end


inline?inline_1(clk,a,b,d1,d2,d);


endmodule

以上代碼對(duì)a&&b分別進(jìn)行了immediate和concurrent assertions,波形顯示兩種斷言結(jié)果完全相同，都在時(shí)鐘上升沿前進(jìn)行采樣。

06 補(bǔ)充知識(shí)點(diǎn)

assert

動(dòng)態(tài)仿真中，如果仿真工具運(yùn)行測(cè)試用例時(shí)發(fā)現(xiàn)斷言失敗，就會(huì)打印出相應(yīng)的信息。

形式化驗(yàn)證中，assertion就是Formal驗(yàn)證工具（例如cadence的jasperGold）的證明目標(biāo)。Formal驗(yàn)證工具會(huì)遍歷所有的合法場(chǎng)景，在數(shù)學(xué)上證明這個(gè)斷言永遠(yuǎn)不會(huì)失敗。還是那句話，仿真只能“證偽” ，而Formal驗(yàn)證具有可以“證明”的能力。

cover

動(dòng)態(tài)仿真中，覆蓋率是一個(gè)非常關(guān)鍵的數(shù)據(jù)，表明驗(yàn)證人員關(guān)注的場(chǎng)景是否真的在用例測(cè)試時(shí)被覆蓋到。通常，需要確保每個(gè)測(cè)試點(diǎn)都至少被覆蓋過(guò)一次，不然就說(shuō)明我們的測(cè)試存在潛在的風(fēng)險(xiǎn)。

形式化驗(yàn)證中，cover也起著重要的作用。盡管理論上Formal覆蓋DUT所有的場(chǎng)景，但是如果我們對(duì)設(shè)計(jì)過(guò)約了，可能還是會(huì)遺漏關(guān)鍵的場(chǎng)景測(cè)試。這時(shí)候，我們?nèi)匀恍枰褂胏over來(lái)證明，我們確實(shí)對(duì)這個(gè)場(chǎng)景進(jìn)行了有效的驗(yàn)證和覆蓋。

assume

動(dòng)態(tài)仿真中，對(duì)于assume和assert的處理是完全相同的。EDA仿真器會(huì)在執(zhí)行測(cè)試用例的時(shí)候檢查assume是否失敗，如果失敗就會(huì)打印相應(yīng)的信息。但是在概念上，assume和assert還是有些區(qū)別的：assume失敗意味著驗(yàn)證環(huán)境或者周邊設(shè)計(jì)可能出現(xiàn)了問(wèn)題，即所測(cè)設(shè)計(jì)激勵(lì)的行為不符合預(yù)期；而assert失敗意味著DUT設(shè)計(jì)的行為不符合預(yù)期。

形式化驗(yàn)證中，assume和assert有著很明顯的區(qū)別。就和字面意思一樣，assume是作為設(shè)計(jì)的約束，會(huì)引導(dǎo)Formal工具產(chǎn)生的合法輸入空間。如果沒(méi)有assume，F(xiàn)ormal工具會(huì)盡可能地遍歷所有的空間，像空氣一樣到達(dá)他能夠觸及的空間。大多數(shù)情況，設(shè)計(jì)都會(huì)使用assume降低FPV的復(fù)雜度。

審核編輯：劉清