SystemVerilogAssertions(SVA)简介_信息与通信_工程

SystemVerilogAssertions测试向量传统上，对被测设计（DUT）的验证都是通过在DUT的输入端口加上具有特定时序激励，然后观察DUT的内部状态变化和最后的输出信号，以确定DUT工作是否正确。这种方法对简单的小规模的设计很有用。•当设计规模变大时，要想使用这种方法来验证DUT是不现实的。因为对于规模大的设计，要想遍历设计将遇到的各种情况，验证其正确性，需要成千上万的特定时序激励。•如果设计稍有一点变动，这些时序激励就得重新编写。•设计的复杂性迫使验证工程师使用随机测试平台来生成更多的验证激励。什么是断言Assertion•断言就是对设计属性（行为）的描述，它是用描述性语言来描述设计的属性。在仿真过程中，如果一个被描述的属性不是我们期望的那样，那么断言就会失败；或者在仿真过程中，如果出现了一个不应该出现的属性，那么断言也会失败。SystemVerilogAssertions•EnhanceSystemVerilogtosupportAssertion-BasedVerificationWhite-box(insideblock)assertionsBlack-box(atinterfaceboundaries)assertions•SyntacticcompatibilityEasytocodedirectlyin-linewithRTL•SupportfordesignandassertionreuseSupportforassertion“binding”todesignfromseparatefile•MonitoringthedesignConcurrent(“standalone”)assertionsProcedural(“embedded”)assertions为什么要使用断言呢？•原有的Verilog语言是一种过程性语言，设计它的目的是用于硬件描述，不是用于仿真验证，因此它不能很好地控制时序。要描述复杂的时序关系，Verilog语言需要编写冗长的代码，很容易出错，且不易维护。•SVA是一种描述性语言，可以完美地描述和控制时序相关的问题，而且语言本身简洁易读，容易维护。•SVA还提供了许多内嵌的函数用于测试特定的时序关系和自动收集功能覆盖率数据。并且当断言失败时，仿真系统会根据失败断言的严重程度来决定是打印一条错误提示信息还是退出仿真过程，便于定位出错的位置。例•如:要验证这样一个属性：“当信号a在某一个时钟周期为高电平时，那么在接下来的2～4个时钟周期内，信号b应该为高电平”。•用Verilog语言描述这样一个属性需要一大段代码，而用SVA描述就只需要几行代码。下面的代码为SVA。propertya2b_p;@(posedgesclk)$rose(a)|-[2:4]$rose(b);endpropertya2b_a:assertproperty(a2b_p);a2b_c:coverproperty(a2b_p);•property和endproperty为SVA的关键字，描述属性。•a2b_p为属性的名字。•$rose为SVA的内嵌函数，用于检查信号的上升沿。•assertproperty也为SVA的关键字，表示并发断•a2b_a为断言的名字，它把属性a2b_p作为参数。•a2b_c为覆盖语句，它用于记录断言的成功。下图为本断言在ModelSim6.1b环境中的仿真波形和断言出错信息。断言分类SVA分为并发断言和即时断言。•并发断言的计算基于时钟周期，在时钟边沿根据变量的采样值计算表达式。•并发断言可以在静态（形式化）验证工具和动态（仿真）验证工具中使用。•上面的例子就是并发断言。•即时断言基于事件的变化，表达式的计算就像Verilog中的组合逻辑赋值一样，是立即被求值的，而不是时序相关的。•必须放在过程块的定义中，只能用于动态仿真。即时断言的例子•例2：always_combimmi_a:assert(a&&b);即时断言被当作过程块的一部分。当信号a或者信号b发生变化时，always_comb块被执行。区别即时断言和并发断言的关键词是“property”。我们在进行时序检查时，通常使用并发断言，而很少使用即时断言。断言的组成和建立过程•任何复杂的时序模型，其功能总是由多个逻辑事件的组合来表示的。这些事件可以是简单的同一时钟沿被求值的布尔表达式，也可以是经过几个时钟周期求值计算得到的事--SVA使用关键字sequence（序列）来表示这些事件。•许多序列可以被有序地组合起来形成设计的属性，--SVA用关键字property来表示属性。最后属性要在断言中被调用才能真正发挥作用。•用覆盖语句来记录断言成功的次数。断言的建立过程为：“编写布尔表达式—编写序列（sequence）－编写属性（property）—编写断言（assertproperty）和覆盖语句（coverproperty）”。sequences1_s;@(posedgesclk)a##1b##4c##[1:5]z;endsequencea1_a:assertproperty(s1_s);假设要检查“信号a在每个时钟上升沿都为高电平，如果信号在任何一个时钟上升沿不为高电平，断言将失败”。这可以通过下面的代码实现：例：sequences1_s;@(posedgesclk)a;endsequencea1_a:assertproperty(s1_s);c1_c:coverproperty(s1_s);•在sclk(0)处，仿真刚开始，a还没有被赋值，为不定态x，所以在sclk(0)处，断言失败。•在sclk(1)处，采样当a为0，断言失败。在其余时钟上升沿处，分析方法类似。•最后断言在第0、1、2、7、12、13、14个时钟上升沿失败，在其余时钟上升沿成功。除了可以使用仿真环境默认的断言错误提示信息外，还可以在断言中添加自己的提示信息。例：sequences1_s;@(posedgesclk)a;endsequencea1_a:assertproperty(s1_s)$display(“assertionsuccess”,$time)else$display(“assertionfaild”,$time);•检查如果信号a在某个时钟周期为高电平，两个时钟周期后信号b也必须为高电平。sequences2_s;@(posedgesclk)a##2b;endsequencea2_a:assertproperty(s2_s);c2_c:coverproperty(s2_s);信号边沿检查SVA提供了3个内嵌函数，用于检查信号的边沿变化。•$rose(布尔表达式或信号名)--当信号/表达式的最低位由0变为1时返回真值。•$fell(布尔表达式或信号名)--当信号/表达式的最低位由1变为0时返回真值。•$stable(布尔表达式或信号名)--当信号/表达式的最低位不发生变化时返回真值。sequencerose_s;@(posedgesclk)$rose(a);endsequencesequencefell_s;@(posedgesclk)$fell(a);endsequencesequencestable_s;@(posedgesclk)$stable(a);endsequencerose_a:assertproperty(rose_s);fell_a:assertproperty(fell_s);stable_a:assertproperty(stable_s)；•rose_a用于检测信号a的上升沿，它只在“a在当前时钟周期为高电平，在前一个时钟周期为低电平”的情况下才成功，如第3、8、11个时钟周期，在其它情况下失败。•fell_a用于检测信号a的下降沿，它只在“a在当前时钟周期为低电平，在前一个时钟周期为高电平”的情况下才成功，如第3、8、11个时钟周期，在其它情况下失败。•在sclk(0)处，采样到a为不定态x。在sclk(1)处，采样到a为0。a从x变到0，本仿真环境认为是a的下降沿，所有断言成功。•stable_a用于检查信号a不变的情况，它只在“a在当前时钟周期为一个电平，在前一个时钟周期也为同样的电平”的情况下成功。如第0、2、4、5、6、8、10、11、13个时钟周期。•在sclk(0)处，采样到a为不定态x，仿真系统认为在0时刻之前a同样为不定态x，所有在sclk(0)处断言成功。蕴含操作符•蕴含操作符的左边项为“先行算子”（antecedent），右边项为“后序算子”（consequent）。•先行算子是约束条件，当先行算子匹配（成功）时，后序算子才能被计算。如果先行算子不成功，那么整个属性就被默认成功，叫“空成功”（vacuoussuccess）。蕴含结构只能被用在属性定义中，不能用在序列定义中。•蕴含操作符分为两类：交叠蕴含操作符（|-）和非交叠蕴含操作符（|=）。•非交叠蕴含操作符“|-”表示：如果先行算子匹配，后序算子在同一个时钟周期开始计算。•交叠蕴含操作符“|=”表示：如果先行算子匹配，后序算子在下一个时钟周期开始计算。propertyoverloap_impli_p;@(posedgesclk)a|-b;endpropertypropertynon_overloap_impli_p;@(posedgesclk)a|=b;Endpropertyoverlap_impli_a:assertproperty(overloap_impli_p);overlap_impli_c:coverproperty(overloap_impli_p);non_overloap_impli_a:assertproperty(non_overloap_impli_p);non_overloap_impli_c:coverproperty(non_overloap_impli_p);•overloap_impli_a用于检测“信号a在某个时钟周期为高电平，并且信号b在同一个时钟周期也为高电平”的情况。整个断言只有在检测到信号a为高电平时才能被激活。在所有被激活的断言中，一共有8次成功，5次失败。•non_overlap_impli_a用于检测“信号a在某个时钟周期为高电平，并且信号b在下一个时钟周期也为高电平”的情况。整个断言只有在检测到信号a为高电平时才能被激活。在所有被激活的断言中，一共有6次成功，6次失败。序列重复操作符•使用序列的重复操作符进行检查序列的重复操作符分为3类：连续重复，跳转重复和非连续重复。•“[*m]”为连续重复操作符。“a[*3]”表示a被连续重复3次，“a[*1:3]”表示a被连续重复1～3次。连续重复的相邻两次重复之间只有一个时钟间隔。•“[-m]”为跳转重复操作符。“a[-3]”表示a被跳转重复3次，“a[-1:3]”表示a被跳转重复1～3次。跳转重复的每一次重复之前可以有任意个时钟周期的间隔。•“[=m]”为非连续重复操作符。“a[=3]”表示a被非连续重复3次，“a[=1:3]”表示a被非连续重复1～3次。非连续重复的每一次重复之前可以有任意个时钟周期的间隔，最后一次重复之后可以有任意个时钟周期的间隔。propertycons_rep_p;@(posedgesclk)$rose(a)|-##1b[*3]##1c;endpropertypropertygoto_rep_p;@(posedgesclk)$rose(a)|-##1b[-3]##1c;endpropertypropertynon_cons_rep_p;@(posedgesclk)$rose(a)|-##1b[=3]##1c;endpropertycons_rep_a:assertproperty(cons_rep_p);cons_rep_c:coverproperty(cons_rep_p);goto_rep_a:assertproperty(goto_rep_p);goto_