01 何為斷言

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

02 斷言的作用

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

· 使用斷言可以使設計中存在的各種問題更容易被動態監測觀察；

· 使用斷言內嵌的覆蓋率統計功能（cover）可以更加容易的獲得對于功能的覆蓋性；

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

· 通過全局控制實現設計中斷言的開關；

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

03 斷言的種類

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

3.1 立即斷言

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

語法：

labels：assert（expression）action_block;

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

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

· action_block: pass_statement; else fail_statement;

例子：

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

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

斷言失敗默認嚴重程度為error，error達到一定數量仿真會退出

立即斷言構建思路：

3.2 并發斷言

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

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

· 并發斷言僅在有時鐘周期的情況下出現

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

· 可以在過程塊、module、interface和program塊內定義并發斷言

· 區別并發斷言和立即斷言的關鍵字是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 斷言層次結構

SVA中可以存在內建的單元，這些單元可以是以下的幾種：

Boolean expressions 布爾表達式

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

Sequence序列

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

Property 屬性

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

4.1 sequence 序列

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

sequence具有如下特性：

? 可帶參數；

? 可以在 property 中調用；

? 可以使用局部變量；

? 可以定義時鐘周期；

sequence的定義格式如下：

sequence name_of_sequence(參數);

……

endsequence

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

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


//2.使用sequence+property實現對a&&b時序的判斷


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


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

sequence 序列可以帶參數：

格式：

sequence seq1(signal1,signal2);

@(posedge clk) signal1&&signal2;

endsequence

用法：

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

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

例如：

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


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

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

sequence 序列可以內嵌

格式：

sequence seq1;

@(posedge clk) a&&b;

endsequence

sequence seq2;

seq1;

endsequence

4.2 property 序列

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

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

格式：

property的定義格式如下：

property name_of_property(參數列表);

測試表達式或復雜的sequence；

endproperty

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

assertion_name: assert property(property_name)

else

$display("SVA error");

并行斷言構建思路：

05 sequence和property的異同

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

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

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

· property需要用cover /assert/assume 等關鍵字進行實例化，而sequence直接調用即可。

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

//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,波形顯示兩種斷言結果完全相同，都在時鐘上升沿前進行采樣。

06 補充知識點

assert

動態仿真中，如果仿真工具運行測試用例時發現斷言失敗，就會打印出相應的信息。

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

cover

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

形式化驗證中，cover也起著重要的作用。盡管理論上Formal覆蓋DUT所有的場景，但是如果我們對設計過約了，可能還是會遺漏關鍵的場景測試。這時候，我們仍然需要使用cover來證明，我們確實對這個場景進行了有效的驗證和覆蓋。

assume

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

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

審核編輯：劉清