《SystemVerilogAssertions(SVA)简介_信息与通信_工程.pdf》由会员分享，可在线阅读，更多相关《SystemVerilogAssertions(SVA)简介_信息与通信_工程.pdf（36页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、 System Verilog Assertions 测试向量 传统上，对被测设计（DUT）的验证都是通过在DUT 的输入端口加上具有特定时序激励，然后观察DUT 的内部状态变化和最后的输出信号，以确定DUT 工作是否正确。这种方法对简单的小规模的设计很有用。当设计规模变大时，要想使用这种方法来验证DUT 是不现实的。因为对于规模大的设计，要想遍历设计将遇到的各种情况，验证其正确性，需要成千上万的特定时序激励。如果设计稍有一点变动，这些时序激励就得重新编写。设计的复杂性迫使验证工程师使用随机测试平台来生成更多的验证激励。什么是断言什么是断言Assertion 断言就是对设计属性（行为）的描述，
2、它是用描述性语言来描述设计的属性。在仿真过程中，如果一个被描述的属性不是我们期望的那样，那么断言就会失败；或者在仿真过程中，如果出现了一个不应该出现的属性，那么断言也会失败。SystemVerilog Assertions Enhance SystemVerilog to support Assertion-Based Verification White-box(inside block)assertions Black-box(at interface boundaries)assertions Syntactic compatibility Easy to code directly i
3、n-line with RTL Support for design and assertion reuse Support for assertion“binding”to design from separate file Monitoring the design Concurrent(“standalone”)assertions Procedural(“embedded”)assertions 为什么要使用断言呢？为什么要使用断言呢？原有的Verilog 语言是一种过程性语言，设计它的目的是用于硬件描述，不是用于仿真验证，因此它不能很好地控制时序。要描述复杂的时序关系，Verilog
4、语言需要编写冗长的代码，很容易出错，且不易维护。SVA 是一种描述性语言，可以完美地描述和控制时序相关的问题，而且语言本身简洁易读，容易维护。SVA 还提供了许多内嵌的函数用于测试特定的时序关系和自动收集功能覆盖率数据。并且当断言失败时，仿真系统会根据失败断言的严重程度来决定是打印一条错误提示信息还是退出仿真过程，便于定位出错的位置。例 如:要验证这样一个属性：“当信号a 在某一个时钟周期为高电平时，那么在接下来的24个时钟周期内，信号b 应该为高电平”。用Verilog 语言描述这样一个属性需要一大段代码，而用SVA 描述就只需要几行代码。下面的代码为SVA。property a2b_p;(
5、posedge sclk)$rose(a)|-2:4$rose(b);endproperty a2b_a:assert property(a2b_p);a2b_c:cover property(a2b_p);property 和endproperty 为SVA 的关键字，描述属性。a2b_p 为属性的名字。$rose 为SVA 的内嵌函数，用于检查信号的上升沿。assert property 也为SVA 的关键字，表示并发断 a2b_a 为断言的名字，它把属性a2b_p 作为参数。a2b_c 为覆盖语句，它用于记录断言的成功。下图为本断言在ModelSim 6.1b 环境中的仿真波形和断言出错
6、信息。断言分类断言分类 SVA 分为并发断言和即时断言。并发断言的计算基于时钟周期，在时钟边沿根据变量的采样值计算表达式。并发断言可以在静态（形式化）验证工具和动态（仿真）验证工具中使用。上面的例子就是并发断言。即时断言基于事件的变化，表达式的计算就像Verilog 中的组合逻辑赋值一样，是立即被求值的，而不是时序相关的。必须放在过程块的定义中，只能用于动态仿真。即时断言的例子即时断言的例子 例2：always_comb immi_a:assert(a&b);即时断言被当作过程块的一部分。当信号a 或者信号b 发生变化时，always_comb 块被执行。区别即时断言和并发断言的关键词是“pr
7、operty”。我们在进行时序检查时，通常使用并发断言，而很少使用即时断言。断言的组成和建立过程断言的组成和建立过程 任何复杂的时序模型，其功能总是由多个逻辑事件的组合来表示的。这些事件可以是简单的同一时钟沿被求值的布尔表达式，也可以是经过几个时钟周期求值计算得到的事-SVA 使用关键字sequence（序列）来表示这些事件。许多序列可以被有序地组合起来形成设计的属性，-SVA 用关键字property 来表示属性。最后属性要在断言中被调用才能真正发挥作用。用覆盖语句来记录断言成功的次数。断言的建立过程为：“编写布尔表达式 编写序列（sequence）编写属性（property）编写断言（as
8、sert property）和覆盖语句（cover property）”。sequence s1_s;(posedge sclk)a#1 b#4 c#1:5 z;endsequence a1_a:assert property(s1_s);假设要检查“信号a 在每个时钟上升沿都为高电平，如果信号在任何一个时钟上升沿不为高电平，断言将失败”。这可以通过下面的代码实现：例：sequence s1_s;(posedge sclk)a;endsequence a1_a:assert property(s1_s);c1_c:cover property(s1_s);在sclk(0)处，仿真刚开始，a 还
9、没有被赋值，为不定态x，所以在sclk(0)处，断言失败。在sclk(1)处，采样当a 为0，断言失败。在其余时钟上升沿处，分析方法类似。最后断言在第0、1、2、7、12、13、14 个时钟上升沿失败，在其余时钟上升沿成功。除了可以使用仿真环境默认的断言错误提示信息外，还可以在断言中添加自己的提示信息。例：sequence s1_s;(posedge sclk)a;endsequence a1_a:assert property(s1_s)$display(“assertion success”,$time)else$display(“assertion faild”,$time);检查如果信
10、号a 在某个时钟周期为高电平，两个时钟周期后信号b 也必须为高电平。sequence s2_s;(posedge sclk)a#2 b;endsequence a2_a:assert property(s2_s);c2_c:cover property(s2_s);信号边沿检查信号边沿检查 SVA 提供了3 个内嵌函数，用于检查信号的边沿变化。$rose(布尔表达式或信号名)-当信号/表达式的最低位由0 变为1 时返回真值。$fell(布尔表达式或信号名)-当信号/表达式的最低位由1 变为0 时返回真值。$stable(布尔表达式或信号名)-当信号/表达式的最低位不发生变化时返回真值。sequ
11、ence rose_s;(posedge sclk)$rose(a);endsequence sequence fell_s;(posedge sclk)$fell(a);endsequence sequence stable_s;(posedge sclk)$stable(a);endsequence rose_a:assert property(rose_s);fell_a:assert property(fell_s);stable_a:assert property(stable_s)；rose_a 用于检测信号a 的上升沿，它只在“a 在当前时钟周期为高电平，在前一个时钟周期为低电平
12、”的情况下才成功，如第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
13、，仿真系统认为在0 时刻之前a 同样为不定态x，所有在sclk(0)处断言成功。蕴含操作符蕴含操作符 蕴含操作符的左边项为“先行算子”（antecedent），右边项为“后序算子”（consequent）。先行算子是约束条件，当先行算子匹配（成功）时，后序算子才能被计算。如果先行算子不成功，那么整个属性就被默认成功，叫“空成功”（vacuous success）。蕴含结构只能被用在属性定义中，不能用在序列定义中。蕴含操作符分为两类：交叠蕴含操作符（|-）和非交叠蕴含操作符（|=）。非交叠蕴含操作符“|-”表示：如果先行算子匹配，后序算子在同一个时钟周期开始计算。交叠蕴含操作符“|=”表示：如果
14、先行算子匹配，后序算子在下一个时钟周期开始计算。property overloap_impli_p;(posedge sclk)a|-b;endproperty property non_overloap_impli_p;(posedge sclk)a|=b;Endproperty overlap_impli_a:assert property(overloap_impli_p);overlap_impli_c:cover property(overloap_impli_p);non_overloap_impli_a:assert property(non_overloap_impli_p);
15、non_overloap_impli_c:cover property(non_overloap_impli_p);overloap_impli_a 用于检测“信号用于检测“信号a 在某个时钟周期为高电平，并且信号在某个时钟周期为高电平，并且信号b 在同一个时钟周期也为高电平”的情况。在同一个时钟周期也为高电平”的情况。整个断言只有在检测到信号整个断言只有在检测到信号a 为高电平时才能被激活。为高电平时才能被激活。在所有被激活的断言中，一共有在所有被激活的断言中，一共有8 次成功，次成功，5 次失败。次失败。non_overlap_impli_a 用于检测“信号用于检测“信号a 在某个时钟周期
16、为高电平，并且信号在某个时钟周期为高电平，并且信号b 在下一个时钟周期也为高电平”的情况。在下一个时钟周期也为高电平”的情况。整个断言只有在检测到信号整个断言只有在检测到信号a 为高电平时才能被激活。为高电平时才能被激活。在所有被激活的断言中，一共有在所有被激活的断言中，一共有6 次成功，次成功，6 次失败。次失败。序列重复操作符序列重复操作符 使用序列的重复操作符进行检查序列的重复操作符分为3 类：连续重复，跳转重复和非连续重复。“*m”为连续重复操作符。“a*3”表示a 被连续重复3 次，“a*1:3”表示a 被连续重复13 次。连续重复的相邻两次重复之间只有一个时钟间隔。“-m”为跳转重
17、复操作符。“a-3”表示a 被跳转重复3 次，“a-1:3”表示a被跳转重复13 次。跳转重复的每一次重复之前可以有任意个时钟周期的间隔。“=m”为非连续重复操作符。“a=3”表示a 被非连续重复3 次，“a=1:3”表示a被非连续重复13 次。非连续重复的每一次重复之前可以有任意个时钟周期的间隔，最后一次重复之后可以有任意个时钟周期的间隔。property cons_rep_p;(posedge sclk)$rose(a)|-#1 b*3#1 c;endproperty property goto_rep_p;(posedge sclk)$rose(a)|-#1 b-3#1 c;endpro
18、perty property non_cons_rep_p;(posedge sclk)$rose(a)|-#1 b=3#1 c;endproperty cons_rep_a:assert property(cons_rep_p);cons_rep_c:cover property(cons_rep_p);goto_rep_a:assert property(goto_rep_p);goto_rep_c:cover property(goto_rep_p);non_cons_rep_a:assert property(non_cons_rep_p);non_cons_rep_c:cover p
19、roperty(non_cons_rep_p);在sclk(3)处a 为高电平，3 个断言都被激活。1 个时钟周期后，b 出现3 次连续的重复，再过1 个时钟周期后，c 为高电平，这样3 个断言都成功。在sclk(10)处a 为高电平，3 个断言都被激活。1 个时钟周期后，b 为低电平，断言cons_rep_a就失败。再过1 个时钟周期，b 出现3 次不连续的重复，再过1 个时钟周期，c 为高电平，这样断言goto_rep_a 和non_cons_rep_a 成功。在sclk(20)处a 为高电平，3 个断言都被激活。1 个时钟周期后，b 为低电平，断言cons_rep_a就失败。再过1 个时钟周期，b 出现3 次不连续的重复，再过1 个时钟周期，c 为低电平，断言goto_rep_a 也失败。最后再过1 个时钟周期，c 为高电平，断言non_cons_rep_a 成功。结论结论 SVA 作为SystemVerilog 语言最重要的内容之一，它可以在以下地方监视信号间的各种时序关系：（1）设计模块的内部；（2）模块与模块间的连接信号；（3）和RTL 代码放在一起进行综合，用于调试；（4）进行设计的功能覆盖。而且SVA 和可综合的RTL 级语言都被统一到了systemVerilog 语言，使得设计工程师和验证工程师可以很好地沟通，方便管理，加快设计进程。