一、SVA是什么

SVA是System Verilog Assertion的縮寫，即用SV語言來描述斷言。斷言是對設(shè)計(jì)的屬性的描述，用以檢查設(shè)計(jì)是否按照預(yù)期執(zhí)行。

斷言常用來驗(yàn)證總線時序或其他特定的時序邏輯，找出設(shè)計(jì)中的違例等。

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

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

格式如下，[ ]內(nèi)為可選內(nèi)容。

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

//如果狀態(tài)為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;

并行斷言：時序性的，需要使用關(guān)鍵詞property，與設(shè)計(jì)模塊并行執(zhí)行，并行斷言只會在時鐘邊沿激活，變量的值是采樣到的值。

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

二、SVA如何使用

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

property property_name;  ;endproperty

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

assertproperty(property_name);

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

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

直接嵌入RTL代碼的module塊中，通常用于設(shè)計(jì)人員；

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

對于驗(yàn)證人員，通常定義一個單獨(dú)的sva模塊，在其中進(jìn)行property的聲明和調(diào)用，然后和DUT或者平臺頂層top進(jìn)行綁定。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具有層次結(jié)構(gòu)，由低到高為布爾表達(dá)式-->序列sequence-->屬性property，sequence描述的是一個時序過程，而property則是某種邏輯狀態(tài)，或者多個時序過程應(yīng)該符合的關(guān)系，也是我們要斷言的對象。sequence和property的區(qū)別如下：

對于較為簡單的時序邏輯關(guān)系，可以不單獨(dú)定義sequence，將sequence的內(nèi)容直接寫在property中；而對于時序關(guān)系較復(fù)雜的，或者為了提高復(fù)用性，可以將一些時序邏輯定義為單獨(dú)的sequence，然后在property中調(diào)用。

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 蘊(yùn)含操作符

蘊(yùn)含操作符只能在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 重復(fù)操作

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

property con_cycle1(a,b);

@ (posedge clk) a[*3];

endproperty

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

property con_cycle2(a,b);

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

endproperty

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

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 同步

默認(rèn)情況下，多重sequence的組合是以后一個sequence的起始時間作為同步標(biāo)志的，SVA提供ended結(jié)構(gòu)以sequence的結(jié)束時間作為序列同步點(diǎn)。

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

sequence s1;

@(posedge clk) a##1 b;

endsequence

sequence s2;

@(posedge clk) c ##1 d;

endsequence

property p1;

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

endproperty

property p2;

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

endproperty

property p3;

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

endproperty

property p4;

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

endproperty

3.6內(nèi)建函數(shù)

四、一些使用技巧

4.1 可變延時范圍

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

如下的操作是非法的：

property variable_delay(cfg_delay);

@(posedge clk) disable iff (!rstn)

a ##cfg_delay b;

endproperty

但是如果我們還是想實(shí)現(xiàn)相同的可變延時，該怎么做呢？

可以定義一個seqence，間接實(shí)現(xiàn)相同的效果。

//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的實(shí)現(xiàn)：

首先定義了一個sequence內(nèi)的局部變量，sequence內(nèi)部是可以定義變量來做輔助邏輯表達(dá)的。

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

(1,delay=v_delay) -> 在序列的起始位置，生成一個事件(1,delay=v_delay),這個事件表示，在第一個時鐘上升沿時，將delay的值設(shè)置為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)重復(fù)若干次，直到delay的值為0. 此處相當(dāng)是一個循環(huán)操作。

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

4.2 Glue Logic

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

如下的一個例子，對interface的SOP和EOP進(jìn)行檢查，DUT規(guī)范要求：

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

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

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

單純用SVA編寫的代碼如下，可以發(fā)現(xiàn)比較復(fù)雜。

sequence sop_seen; //當(dāng)sop出現(xiàn)后，該序列會持續(xù)成立

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之前或者當(dāng)拍一定有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]))

);

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

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拍之前或者當(dāng)拍一定有sop

vld && eop |-> in_packt || sop

);

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

vld && sop |-> !in_packet

);