01 何為斷言

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

02 斷言的作用

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

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

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

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

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

· 斷言可以加速形式驗證，提高形式驗證的效率；

03 斷言的種類

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

3.1 立即斷言

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

語法：

labels：assert（expression）action_block;

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

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

· 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達到一定數(shù)量仿真會退出

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

3.2 并發(fā)斷言

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

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

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

· 測試表達式是基于所涉及變量的采樣值在時鐘邊緣進行計算的

· 可以在過程塊、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 布爾表達式

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

Sequence序列

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

Property 屬性

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

4.1 sequence 序列

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

sequence具有如下特性：

? 可帶參數(shù)；

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

? 可以使用局部變量；

? 可以定義時鐘周期；

sequence的定義格式如下：

sequence name_of_sequence(參數(shù));

……

endsequence

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

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


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


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");

帶時序關(guān)系的sequence ：在SVA中時鐘延時用符號"##"來表示，如"##2"表示延時兩個時鐘周期；

例如：

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


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

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

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

格式：

sequence seq1;

@(posedge clk) a&&b;

endsequence

sequence seq2;

seq1;

endsequence

4.2 property 序列

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

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

格式：

property的定義格式如下：

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

測試表達式或復(fù)雜的sequence；

endproperty

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

assertion_name: assert property(property_name)

else

$display("SVA error");

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

05 sequence和property的異同

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

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

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

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

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

//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

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

06 補充知識點

assert

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

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

cover

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

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

assume

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

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

審核編輯：劉清