基于断言语言SVA的设计验证方法

摘 要:基于断言SVA的验证是一种有价值的主流验证技术。断言特别适合于描述时序特性和因果特性。作为System Verilog的重要组成部分,SVA提供了丰富的断言指令,能有效地提高验证测试工作的质量和效率。在此,首先介绍断言验证语言SVA,通过与Verilog验证对比,说明SVA在时序特性和因果特性验证上的优势,证明基于断言的验证是SoC设计验证的一种有效方法,能够有效地提高验证效率。

关键词:验证方法; SVA; 时序特性; 因果特性

中图分类号:TN710 文献标识码:A

文章编号:1004-373X(2010)10-0005-03

Verification Method of SVA Language

ZHA Xin

(Shanghai Jiaotong University, Shanghai 200335, China)

Abstract: Verification based on SVA(system verilog assertion) is a valuable mainstream verification technology. SVA is especially propitious to the description of time-sequence characteristics and causality. As an important part of SystemVerilog, SVA which can effectively improve the quality and efficiency of verification work provides abundant assertion instructions. In this paper, the assertion language SVA is introduced, and an example verified by Verilog and SVA is provided to describe the preponderance of SVA in time-sequence characteristics and causality. It proves that SVA verification is a effective method for SoC design verification, and can improve the verification efficiency.

Keywords: verification; method; SVA; time-sequence charouteristic; causal property

0 引 言

随着芯片设计规模的不断扩大,以及设计复杂度的上升,SoC设计技术已经成为一种发展趋势。根据Collett国际公司2003年的调查,造成芯片流片失败的原因有很多,其中大约有70%的原因是来自于SoC设计本身的功能验证不足[1]。

SoC设计需要面对的瓶颈已不再是设计时间,而是验证时间,验证工作已经占到了整个项目工作量的70%以上,保证芯片功能的正确性已成为SoC和ASIC设计中的最大挑战。同时,也出现了许多新的验证方法和理论,如基于断言的验证、覆盖率导向的验证、可约束的随机激励、事务级验证等[2-5]。其中,基于断言的验证是硬件设计功能验证的一种有效方法。

作为一种对设计对象的属性或行为特性的描述,断言并不是新的概念。随着硬件描述语言应用于硬件设计,断言的方法也被引入设计验证当中。VHDL语言中的关键词Assert使设计者可以在代码中方便地加入断言;各种新的验证语言,如Vera,PSL以及SystemVerilog对断言都有更好的支持[3,6-7]。随着硬件描述语言Verilog的广泛应用,SVA(system verilog assertion)在设计验证中越来越被重视和应用。另外,各种仿真工具对Verilog和System Verilog的支持,尤其是断言在形式验证中的应用,使基于断言语言SVA的验证方法在设计验证中发挥了越来越重要的作用。

1 基于断言语言SVA的验证方法

1.1 断言语言SVA

Accellera委员会已经将Systerm Verilog 3.1定为一个标准,断言语言被纳入System Verilog,成为标准的一部分,即SVA。SVA允许把断言应用到设计中的一系列工具,它具有丰富的语法,可在序列和断言中支持时间概念。设计者可以对硬件的期待进行编码,可以创建对硬件功能设计的详细验证。

对于一个设计模型的功能,可以用多个可能的逻辑事件之组合来表达。这些事件可以是在同一个时钟周期边缘被求值,也可以经过多个时钟周期之后求值。SVA中用序列对时态行为逻辑事件组合进行仿真。序列是一个以时间为序的布尔表达式列表。用关键词:“sequence”来定义。对于复杂的有序行为,可以在属性(property)的定义中描述。在property的定义中,可以将多个序列逻辑或时序地组合起来生成更复杂的序列,以表达复杂的有序行为[8]。

序列sequence的语法格式如下:

sequence names;

;

endsequence

属性property的语法格式如下:

property namep;

;or

;

endproperty

属性是仿真过程中被检验的单元,它必须在仿真过程中用断言来发挥作用。SVA提供关键词“assert”来检查属性。建立属性并对其断言的步骤如图1所示。

图1 建立属性并对其断言的步骤

SVA中有2类断言:实时断言和并发断言。实时断言遵循仿真事件执行时的语义,它们是带有System Verilog关键词Assert作为前导的Verilog过程语句。实时断言在过程仿真中具有立即求值特性;并发断言使用顺序结构描述时态行为,可以在任何位置调用。以下是并发断言和实时断言的例子:

Abf:assert property (@posedge clk) not (a && b));//并发断言

Ajs:assert (a && b);//实时断言

关键词property区分并发断言与实时断言。

1.2 使用断言语言SVA验证的好处

使用断言的最大好处是为SoC设计验证提供了良好的可观察性,可以比较容易地发现潜在电路设计的内部错误。传统的验证方法是首先产生适当的激励输入到DUV(design under verification)中,然后在输出端口确认数据传输的正确性。同时,也存在着这样一种可能性,即产生的输入激励触发了某种设计漏洞,但这种错误并没有传递到设计的输出端。如果在验证代码中嵌入断言,就可以在更接近产生漏洞的地方将其检测出来。

另外,断言SVA验证提供了良好的可控制性,可以产生多且有效的测试向量,提高电路验证功能的正确性。在验证过程中,可以覆盖电路各种可能发生例外的情况,提高验证效率。

使用断言SVA验证可以对一个给定输入的设计期望行为进行精确的描述,从而可以更方便地描述输入/输出行为、总线协议以及设计中一些复杂的关系。基于断言的验证语言,SVA可以使用简洁的语言结构来建立精确的时序表达式。通过检查这些表达式是否发生,可以很简单地进行功能覆盖的检查,并且这种覆盖率分析针对跨多个时序周期的一个时间序列或者个传输。传统覆盖分析要专门为覆盖分析而写大量的代码,而断言的覆盖分析可以直接使用在协议检查或者事件描述中用到的时序表达式,因此编码会更加灵活、简洁。

2 举例说明

采用一个简单的时序为例,通过传统硬件描述语言Verilog的验证设计与断言语言SVA的验证设计进行比较,说明SVA在验证中的简洁、精确描述。

在SoC的设计中,很多模块都会与memory有数据传输,在与memory的bus线上一定有输入到memory的时钟信号(如图2中的spidmack),以及选择信号(spidmacs)和读使能信号(spidmard)。

图2 时序要求

从图2所示的波形图来看,spidmacs和spidmard信号都以spidmack为周期的,并且spidmacs和spidmard都是只有1个时钟周期,并且在时序上spidmard要比spidmacs晚1个时钟周期。

用Verilog来设计验证,首先spidmacs信号和spidamrd信号分别需要一个计数器(cscnt & rdcnt),用以保证spidmacs和spidmard信号的周期数为1。另外需要┮桓龆spidmard的检测控制信号(csrdctrl),这个信号是控制spidmard信号是否在spidmacs信号后1个周期产生,并且这个控制信号的时钟周期数必须为1,这才符合时序要求。最后,需要一个判断是否有错的判断信号(csrderror)。具体设计如下:

reg [1:0] cscnt;

always@(posedge spidmack,posedge rstsva)

begin

if(rstsva) cscnt

else if(spidmacs) cscnt

else if(~spidmacs) cscnt

end

cscnt信号是对spidmacs为“1”的计数,如果spidmacs为“0”,cscnt会自动清为0。

Reg [1:0] rdcnt;

always@(posedge spidmack,posedge rstsva)

begin

if(rstsva) rdcnt

else if(spidmard)rdcnt

else if(~spidmard) rdcnt

end

rdcnt信号是对spidmard为“1”的计数,如果spidmard为“0”,rdcnt会自动清为0。

Reg csrdctrl;

always@(posedge spidmack,posedge rstsva)

begin

if(rstsva) csrdctrl

else if(spidmacs && (~spidmard)) csrdctrl

else if((~spidmacs) && spidmard) csrdctrl

end

csrdctrl信号在spidmacs为“1”且spidmard为“0”时,置为“1”;在spidmacs为“0”且spidmard为“1”时,清为“0”,这个信号是表示从spidmacs为“1”到spidmard为“1”的过程。要确定这个过程的时间间隔是1个周期,这就必须有1个计数器对其进行计数,用计数器的值来判断是否满足1个周期的时序要求。计数器设计如下:

reg [1:0] csrdcnt;

always@(posedge spidmack,posedge rstsva)

begin

if(rstsva) csrdcnt

else if(csrdctrl) csrdcnt

else if(~csrdctrl) csrdcnt

end

要检测spidmacs和spidmard信号是否符合时序要求,还必须建立查错机制,也就是检测错误的判断,设计如下:

reg csrderror;

always@(posedge spidmack,posedge rstsva)

begin

if(rstsva) csrderror

else if(spidmacs && spidmard) csrderror

else if((cscnt == 2′h2) || (rdcnt == 2′h2) ||

(csrdcnt == 2′h2))

csrderror

else if(csrderror) csrderror

end

从上面verilog的设计可以看出,为了验证spidmacs和spidmard信号的时序,Verilog用了5个always语句来实现。一旦这2个信号在设计时序上有变动,则在Verilog设计验证代码的维护和修改上也将与这5个always语句有关,代码量是很大的。

基于断言语言SVA的详细验证设计如下:

property pcsrd;

@(posedge spidmack)

MYMrose (spidmacs) |->

(!spidmard) ##1 (spidmard && (!spidmacs)) ##1 (!spidmard);

endproperty

acsrd : assert property (pcsrd);

这个属性描述的是以spidmacs的上升沿为触发点的。在spidmacs为“1”的同时,spidmard为“0”,1个时钟周期后,spidmacs为“0”且spidmard为“1”,再1个时钟周期后spidmard为“0”。SVA提供的断言字assert,若断言满足属性(property)中的时序要求,则判断成功,否则判断失败。

上述用SVA语言描述在VCS仿真环境下的仿真结果如图3所示,黑粗线表示上述断言发生。

图3 仿真结果

3 仿真结果

从上面的设计比较可以看出,Verilog作为一种过程语言不能很好地控制时序,并且语言的过程性使得测试在同一时间段内发生的并行事件相当困难。随着检验数量的增加,维护代码将变得很困难,而且Verilog语言没有提供内嵌的机制来提供功能覆盖的数据,必须自己设计实现这部分代码。

SVA是一种描述性语言,可以很好地描述时序相关的状况,语言描述性本质使的能够对时间实现卓越的控制。SVA代码的简洁实现,使得描述精确,易于维护,且SVA提供内嵌函数来测试特定的设计情况,并且提供了一些构造来自动收集功能覆盖数据。

4 结 语

基于断言语言SVA的验证方法,有着传统验证所无法比拟的优势。SVA对待测模块信号间时序关系上描述的便利性,大大提高了模块功能验证的效率,保证了模块功能的正确性,提高了被验证模块的可观性和可控性。利用SVA断言验证能够在错误发生时将其及时捕获,允许设计人员迅速明确发生错误的设计段落,从而大大简化了纠错工作,帮助设计者调整设计,缩短开发周期。

参考文献

[1]张志敏,傅亮.SoC设计验证技术发展综述[EB/OL].[2004-04-06]..

[2]丁婷婷,申敏.分层式验证平台及覆盖率技术在SoC上的应用[J].北京电子科技学院学报,2007,15(2):55-57.

[3]马博,韩俊刚.采用PSL的基于断言的验证[J].计算机工程,2007(2):217-219.

[4]刘有耀,韩俊刚.基于事务断言验证及SDH芯片验证平台[J].微计算机信息,2007,23(14):310-312.

[5]杨|,罗春,杨军.基于矢量随机生成和断言的LCD控制器的验证[J].电子工程师,2006(3):4-6.

[6]刘晓,杨军.基于断言的SRAM控制器功能验证[J].电子工程师,2007(2):23-25.

[7]慕长林.断言验证技术在VERA中的应用与研究[J].科技资讯,2009(1):20.

[8]VIJAYARAGHAVAN Srikanth, RAMANATHAN Mey-yappan. System Verilog Assertions应用指南[M].陈俊杰,译.北京:清华大学出版社,2006.

[9]闫沫,张媛.基于System Verilog语言的设计验证技术[J].现代电子技术,2008,31(6):8-11.

[10]徐中伟,李海波.面向断言的测试数据生成方法及其应用[J].同济大学学报:自然科学版,2007(7):659-663.

[11]刘有耀,韩俊刚.属性说明语言在基于断言的硬件验证中的应用[J].微电子学与计算机,2006,23(5):109-111,114.

[12]徐盛,章玮,金钊.基于断言的验证方法在总线协议验证中的应用[J].电子设计应用,2006(11):88-90.

[13]FOSTER Harry, KROLNIK A, LACEY D. Assertion based design[M]. 2nd ed. New York: Kluwer Academic Publishers, 2004.

[14]劳丰,郭立.断言语言SVA在硬件功能验证中的应用[J].电子技术,2008,45(7):45-47.