一、SVA是什么

SVA是System Verilog Assertion的縮寫，即用SV語言來描述斷言。斷言是對設計的屬性的描述，用以檢查設計是否按照預期執行。

斷言常用來驗證總線時序或其他特定的時序邏輯，找出設計中的違例等。

斷言可以分為立即斷言和并行斷言兩種常見類型。

立即斷言：非時序，執行時如同過程語句，可以在initial/always過程塊或者task/function中使用。立即斷言可以結合$fatal、$error、$warning、$info給出不同嚴重等級的消息提示。

格式如下，[ ]內為可選內容。

[name:]assert(expression)[pass_statement][else fail_statement];

//如果狀態為REQ，但是req1或者req2均不為1時，斷言將失敗

always @ (posedge clk) begin

if(state == REQ)

assert(req1||req2) //立即斷言

else begin

t = $time;

#5$error("assert failed at time %0t", t);

end

end

always @ (state)

assert (state == $onehot) else $fatal;

并行斷言：時序性的，需要使用關鍵詞property，與設計模塊并行執行，并行斷言只會在時鐘邊沿激活，變量的值是采樣到的值。

立即斷言很簡單，無需贅述，本文主要講述并行斷言的用法。

二、SVA如何使用

SVA使用"assert"關鍵詞來表示一個斷言屬性。而在進行對屬性斷言之前，我們需要進行屬性(property)的聲明。

property property_name;  ;endproperty

聲明之后便可以對property進行斷言，即 認為property中描述的屬性為真，否則斷言失敗。

assertproperty(property_name);

以上是單獨寫一個property描述時序，然后assert調用它，對于較為簡單的時序，也可直接在括號內寫上property的內容。而對于較復雜的時序，也可以寫定義序列sequence，再由sequence組成property.

SVA用在哪里呢？主要有2種：

直接嵌入RTL代碼的module塊中，通常用于設計人員；

module fifo(input clk, rst_n, read, output empty, ...)

//Actual FIFO code:

...

//Assertion: FIFO must not underflow

input_no_underflow: assert property( @(posedge clk) !(read && empty));

endmodule

對于驗證人員，通常定義一個單獨的sva模塊，在其中進行property的聲明和調用，然后和DUT或者平臺頂層top進行綁定。module fifo_checker (input clk, rst_n, read, empty);

//FIFO must not underflow

input_no_underflow: assert property ( @(posedge clk) !(read && empty) );

endmodule

bind fifo fifo_checker fifo_checker_inst(.clk(clk),.rst_n(rst_n),.read(read),.empty(empty));

三、SVA語法簡介

SVA具有層次結構，由低到高為布爾表達式-->序列sequence-->屬性property，sequence描述的是一個時序過程，而property則是某種邏輯狀態，或者多個時序過程應該符合的關系，也是我們要斷言的對象。sequence和property的區別如下：

對于較為簡單的時序邏輯關系，可以不單獨定義sequence，將sequence的內容直接寫在property中；而對于時序關系較復雜的，或者為了提高復用性，可以將一些時序邏輯定義為單獨的sequence，然后在property中調用。

logic clk = 0;

logic req,gnt;

logic a,b;

//=================================================

// Sequence Layer with args (NO TYPE)

//=================================================

sequence notype_seq (X, Y);

(~X & Y) ##1 (~X & ~Y);

endsequence

//=================================================

// Sequence Layer with args (NO TYPE)

//=================================================

sequence withtype_seq (logic X, logic Y);

(~X & Y) ##1 (~X & ~Y);

endsequence

//=================================================

// Property Specification Layer

//=================================================

property req_gnt_notype_prop(M,N);

@ (posedge clk)

req |=> notype_seq(M,N);

endproperty

property a_b_type_prop(logic M, logic N;

@ (posedge clk)

a |=> withtype_seq(M,N);

endproperty

//=================================================

// Assertion Directive Layer

//=================================================

req_gnt_notype_assert : assert property (req_gnt_notype_prop(req,gnt));

a_b_type_assert : assert property (a_b_type_prop(a,b));

3.1 蘊含操作符

蘊含操作符只能在property中使用。

3.2 延時操作符

用##操作符來表示延時。

logic clk = 0;

logic req,gnt;

logic a,b;

//=================================================

// Sequence Layer with args (NO TYPE)

//=================================================

sequence notype_seq (X, Y);

(~X & Y) ##1 (~X & ~Y);

endsequence

//=================================================

// Sequence Layer with args (NO TYPE)

//=================================================

sequence withtype_seq (logic X, logic Y);

(~X & Y) ##1 (~X & ~Y);

endsequence

//=================================================

// Property Specification Layer

//=================================================

property req_gnt_notype_prop(M,N);

@ (posedge clk)

req |=> notype_seq(M,N);

endproperty

property a_b_type_prop(logic M, logic N;

@ (posedge clk)

a |=> withtype_seq(M,N);

endproperty

//=================================================

// Assertion Directive Layer

//=================================================

req_gnt_notype_assert : assert property (req_gnt_notype_prop(req,gnt));

a_b_type_assert : assert property (a_b_type_prop(a,b));

3.3 重復操作

//連續3個時鐘a均成立，則斷言成功

property con_cycle1(a,b);

@ (posedge clk) a[*3];

endproperty

//a成立3次后(不要求連續)，在下一個時鐘b成立則斷言成功

property con_cycle2(a,b);

@ (posedge clk) a[->3]b;

endproperty

//a成立3次后(不要求連續)，b成立(后續任意一時鐘)

property con_cycle3(a,b);

@ (posedge clk) a[=3]b;

endproperty

3.4 匹配操作

舉例說明first_match(seq)的使用：

seq_a再clk 3 4 5時刻均滿足，但是assert(first_match(seq_a))僅會在clk 3時成功匹配一次，之后便不再檢測。

sequence seq_a;

a[*1:2] ##1 b[*2:3];

endsequence

property first_match_property;

first_match(seq_a);

endproperty

3.5 sequence 同步

默認情況下，多重sequence的組合是以后一個sequence的起始時間作為同步標志的，SVA提供ended結構以sequence的結束時間作為序列同步點。

若使用ended，則sequence必須定義時鐘。關鍵字ended存儲一個反映在指定時鐘處序列是否匹配成功的布爾值。該布爾值僅在同一時鐘內有效。

sequence s1;

@(posedge clk) a##1 b;

endsequence

sequence s2;

@(posedge clk) c ##1 d;

endsequence

property p1;

s1|=>s2; //s1的成功匹配點滯后一時鐘周期是s2匹配的起點

endproperty

property p2;

s1|=>##1 s2.ended; //s1成功匹配點滯后兩個時鐘周期是s2成功匹配點，即s1匹配成功則再過兩個時鐘周期s2必須匹配成功

endproperty

property p3;

s1.ended|=>s2; //s1的成功匹配點滯后一時鐘周期是s2匹配的起點

endproperty

property p4;

s1.ended|=> ##1 s2.ended;//s1成功匹配點滯后兩個時鐘周期是s2成功匹配點，即s1匹配成功則再過兩個時鐘周期s2必須匹配成功

endproperty

3.6內建函數

四、一些使用技巧

4.1 可變延時范圍

延時操作或者重復范圍（即 ##n 或 a[*n]）只可以使用常數，不可以使用變量。

如下的操作是非法的：

property variable_delay(cfg_delay);

@(posedge clk) disable iff (!rstn)

a ##cfg_delay b;

endproperty

但是如果我們還是想實現相同的可變延時，該怎么做呢？

可以定義一個seqence，間接實現相同的效果。

//delay sequence

sequence delay_seq(v_delay);

int delay;

(1,delay=v_delay) ##0 first_match((1,delay=delay-1) [*0:$] ##0 delay <=0);

endsequence

//calling assert property

a_1: assert property(@(posedge clk) a |-> delay_seq(cfg_delay) |-> b);

使用delay_seq來替代變量cfg_delay. 下面解釋這個seqence的實現：

首先定義了一個sequence內的局部變量，sequence內部是可以定義變量來做輔助邏輯表達的。

int delay -> 定義了一個整型變量delay，用于存儲當前的延遲時間。

(1,delay=v_delay) -> 在序列的起始位置，生成一個事件(1,delay=v_delay),這個事件表示，在第一個時鐘上升沿時，將delay的值設置為v_delay。

(1,delay=delay-1) -> (1,delay=delay-1)表示在每個時鐘上升沿時，將delay的值減 1。

first_match((1,delay=delay-1) [*0:$] ##0 delay <=0) ? -> 對事件(1,delay=delay-1)重復若干次，直到delay的值為0. 此處相當是一個循環操作。

綜上所述，這個序列表示：在第一個時鐘上升沿時，將delay的值設置為v_delay，然后每個時鐘上升沿時，將delay的值減 1，直到delay的值小于等于 0。

4.2 Glue Logic

在驗證或建模復雜行為時，引入輔助邏輯來觀察和跟蹤時間可以大大簡化編碼，這種輔助邏輯通常稱為"glue logic".

如下的一個例子，對interface的SOP和EOP進行檢查，DUT規范要求：

packets不能重合（SOP-EOP始終是匹配的）

允許單拍packet（SOP和EOP在同一cycle）

packet是連續的（SOP-EOP之間vld不能有缺口）

單純用SVA編寫的代碼如下，可以發現比較復雜。

sequence sop_seen; //當sop出現后，該序列會持續成立

sop ##1 1'b1[*0:$];

endsequence

no_holes: assert property(//sop 到 eop之間的vld一直有效

sop |-> vld until_with eop

);

sop_first: assert property (vld && eop |-> sop_seen.ended); //eop之前或者當拍一定有sop

eop_correct: assert property(

not (!sop throughout ($past(vld && eop) ##0 vld && eop[->]) )

);

sop_correct: assert property(

vld && sop && !eop |=> not(!$past(vld && eop) throughout (vld && sop[->1]))

);

可已采用一些中間變量進行輔助，這樣可以更簡潔。

reg in_packet;//中間變量

always @(posedge clk) begin

if(!rstn || (eop&&vld) )

in_packet <= 1'b0;

else if (sop&&vld) in_packet <= 1'b1;

end

no_holes: assert property( //中間不能有空缺

in_packet |-> vld

);

eop_correct: assert property( //eop拍之前或者當拍一定有sop

vld && eop |-> in_packt || sop

);

sop_correct: assert property( //不會有重復sop拍

vld && sop |-> !in_packet

);