验证--断言课件

1、SystemVerilog断言（SVA）应用说明,中科院自动化所集成中心 2014-02-11,断言是什么,断言就是对设计属性（行为）的描述，它是用描述性语言来描述设计的属性,比如：ack信号在req信号的1-3个周期内应答,主题列表,断言的说明及其重要性 断言介绍 即时断言 并发断言 断言该放在何处 谁来定义断言 开发断言计划 设计工程师关注的断言 验证工程师关注的断言 断言使用特别说明,断言重要性,为测试平台提供优秀的自检机制 提高验证效率 减少调试时间 提高验证的可观测性和可控性,断言的目的,断言的功能,断言的优势,协议检查 检查设计中控制信号的正确性 数据检验（协议覆盖） 检验正在处理

2、数据的完整性,白盒子模式的验证技术 仿真过程中，自动检测设计错误，并报告详细信息 可用形式化验证工具验证模型是否和断言相符 可报告“约束随机验证”覆盖设计边角的程度,谁定义断言，仅仅验证工程师？,设计工程师也要设计断言 设计的所有假定 模块输入的非法值 所有的握手应该完成 Case语句不会发生不想要的分支 设计工程师在编写RTL时应该增加如下断言 比如假定的情况： 输入没有x值 不会出现未规划状态机序列 在申请信号之后会出现应答信号,验证工程师定义的断言,验证工程师需要验证设计功能满足设计规范 比如当ALU计算输出为0时，ALU的zero 标志信号必须为0 验证不能重复RTL逻辑 RTL：检测

3、输入，给出输出 断言：检测输出，验证输入情况,断言的测试计划的例子,if(wr) begin addr_never_x: assert (addr != 1bx); end,设计断言和RTL的区别： RTL：检测输入，给出输出 断言：检测输出，验证输入情况,SystemVerilog的两种断言,即时断言-在当前时刻测试信号的数值情况,always (state) assert (state = $onehot) else $fatal;,如果不是独热码值，那么会产生严重错误,即时断言相当于一个if .else语句 ，但有断言控制,并发断言-在多个时钟周期测试事件序列的正确性,一个复杂的序列可以

4、用几个简单的代码来定义,即时断言,即时断言的特点： 基于模拟时间的语句 立即求值，和时序无关 必须放在过程块中，比如task，function，initial或者always块 只能用于动态模拟,断言的名称（assert_foo）可以用%m来引用,即时断言格式： name: assert (expression) pass_statement else fail_statement,例子： always_comb begin assert_foo : assert(foo) $display(%m passed); else $display(%m failed); end 或者：assert

5、 (myfunc(a,b) count1 = count + 1; else -event1 或者：assert (y = 0) else flag = 1;,并发断言,即时断言的特点： 基于时钟周期 时钟边沿根据调用变量的采样值计算测试表达式 可以被放在过程块、模块、接口、程序中 可以在静态或者动态验证工具中使用 变量采样在预备阶段完成，表达式计算在观察阶段完成,即时断言格式： name: assert property (property_specification) pass_statement else fail_statement,property_specification表示事件

6、的序列,例子： always (posedge clock) if (State = FETCH) ap_req_gnt: assert property (p_req_gnt) passed_count+; else $fatal; property p_req_gnt; (posedge clock) request #3 grant #1 !request #1 !grant; endproperty:p_req_gnt,$fatal (finish_number,message message_arguments ) 仿真工具终止 finish_number可以是0,1,2 控制工具打

7、印的信息 $error (message message_arguments ) 运行出现严重错误，软件继续执行 $warning (message message_arguments ) 运行出现警告，软件继续执行 $info (message message_arguments ) 不严重，仅仅打印信息,报告严重级别Severity level,如果else语句没有编写的话，工具缺省调用$error,或者通过工具设置,# IgnoreNote = 0 # IgnoreWarning = 0 # IgnoreError = 0 # IgnoreFailure = 0 # IgnoreSVAI

8、nfo= 0 # IgnoreSVAWarning = 0 # IgnoreSVAError = 0 # IgnoreSVAFatal = 0,SystemVerilog支持的断言类别,不变的断言 Invariant 一个条件一直为真（或者不会为真） 例子：FIFO不会同时发生满和空的行为 序列断言 Sequential 在定义的时钟周期内以特殊的顺序发生一组状态 比如request 发起1-3周期后grant必须响应 偶然性断言 Eventuality 在一定的时钟周期内，一种状态跟随另外一种状态 比如：reset变低，可能会变高,断言定义的位置,嵌入到RTL代码中 如同普通程序语句，内嵌到

9、RTL中 综合时会被忽略 在设计模型中，但在独立的并非代码块中 仿真时和设计代码同时执行 综合时会被忽略 在设计模型外，在独立的文件中 可以限定到设计模型指定的实例 仿真时和设计代码同时执行 允许验证工程师方便的修改断言 综合时不用断言文件,并发断言语句的结构,assert property (posedge clk) req |- gnt #1 (done ,序列 sequence,属性property,assert断言 assume 假定 cover覆盖 expect 例外,序列 sequence 一个时钟边沿或者多个时钟周期的求值事件 可以定义在module、interface、prog

10、ram、 clocking block 、package 、compilation-unit scope 属性 property 多个序列逻辑地或者有序地组合起来的复杂序列 可以定义在module、interface、program、 clocking block 、package 、compilation-unit scope 检查属性 property assert断言 assume 假定 cover覆盖 expect 例外 如同普通程序语句，内嵌到RTL中 综合时会被忽略 在设计模型中，但在独立的并非代码块中 仿真时和设计代码同时执行 综合时会被忽略 在设计模型外，在独立的文件中 可以限

11、定到设计模型指定的实例 仿真时和设计代码同时执行 允许验证工程师方便的修改断言 综合时不用断言文件,可执行的例子,module andor; logic a,b,c,d,e; logic clk; initial begin end sequence s27a; (posedge clk) a#1:2 b; endsequence sequence s27b; (posedge clk) c#2:3 d; endsequence property p27; (posedge clk) s27a and s27b; endproperty a27: assert property(p27); e

12、ndmodule,定义不是延时，而是代表#针对哪个时钟,采样数据的函数,这些函数不仅可使用在断言中，在普通程序代码中也可以使用,(posedge clk) $rose(req); (posedge clk) $fell(ack);,$sampled(expression , clocking_event) 采样上一个周期表达式的值，仿真时第一个时钟周期结果是X $rose( expression , clocking_event) 信号或者表达式的最低位变成1时返回真 $fell( expression , clocking_event) 信号或者表达式的最低位变成0时返回真 $stable(

13、 expression , clocking_event) 信号或者表达式不变时返回真,可用于断言的系统函数,$onehot () 独热码 在给定的时钟沿，表达式只有一位为高 $onehot0()独热码和0 在给定的时钟沿，表达式至多有一位为高 $isunknown () 出现未知值 检验表达式的任何位是否为X或者Z $countones ( expression) 统计1数目 计算向量中为高的位的数量,$past获取几个周期之前的值,格式： $past (signal_name, number of clock cycles) $past( expression1 , number_of_t

14、icks , expression2 , clocking_event),例子： property p19; (posedge clk) (c ,增加门控信号$past (signal_name, number of clock cycles , gating signal),posedge clk) (c ,门控表达式,可选，基于的时钟事件,缺省为1,序列的声明,sequence_expr := cycle_delay_range sequence_expr cycle_delay_range sequence_expr | sequence_expr cycle_delay_range s

15、equence_expr cycle_delay_range sequence_expr | expression_or_dist boolean_abbrev | ( expression_or_dist , sequence_match_item ) boolean_abbrev | sequence_instance sequence_abbrev | ( sequence_expr , sequence_match_item ) sequence_abbrev | sequence_expr and sequence_expr | sequence_expr intersect seq

16、uence_expr | sequence_expr or sequence_expr | first_match ( sequence_expr , sequence_match_item ) | expression_or_dist throughout sequence_expr | sequence_expr within sequence_expr | clocking_event sequence_expr,#2 延时周期,sequence_declaration := sequence sequence_identifier ( list_of_formals ) ; asser

17、tion_variable_declaration sequence_expr ; endsequence : sequence_identifier ,Backus-Naur Form (BNF)格式,关键字红色粗体 | 只能选其一 可选项 可重复0或者多个,expression_or_dist := expression dist dist_list boolean_abbrev := consecutive_repetition | non_consecutive_repetition | goto_repetition,consecutive_repetition := * const

18、_or_range_expression non_consecutive_repetition := = const_or_range_expression goto_repetition := - const_or_range_expression ,sequence_match_item := operator_assignment | inc_or_dec_expression | subroutine_call,= | += | -= | *= | /= | %= | 其他例子：a *3 、 (a #1:4 b) *3,跳转（跟随）重复 一个信号或者序列在指定周期内匹配n次，但不一定在

19、连续的时钟周期上发生 a-n等价 (!a) * 0:$ #1 a) *n (posedge clk) $rosestart) |- #2 (a-3) #1 stop;,非连续重复运算符 a=n等价 ( (!a) * 0:$ #1 a #1 (!a) * 0:$)*n (posedge clk) $rose(start) |- #2 a=3) #1 stop #1 !stop;,Intersect 交集,两个序列必须相同时刻开始，并结束与同一个时刻,sequence s28a; (posedge clk) a#l:2 b; endsequence sequence s28b; (posedge

20、clk) c#2:3 d; endsequence property p28; posedge clk) s28a intersect s28b; endproperty,(posedge clk) 1*3:5 intersect (a #1:$ b #1:$ c);,定义了从序列有效点a=1到c=1一共经过了25个周期,可以有效的控制序列的长度,throughout贯穿和within蕴涵,property p31; posedge clk) $fell(start) |- !start) throughout #1 (!a,检查a和b下降沿与信号a和b的上升沿之间，信号c连续或者间断的出现3

21、次高电平,sequence s32a; (posedge clk) (!a,贯穿： 后一个算子计算时前面的算子一直保持为真,蕴涵： 允许一个序列中定义了另外一个序列,未完成：16下降沿，21上升沿，c分别重复了两次高电平，c是跟随重复表达式,first_match第一次序列匹配,sequence s30a; posedge clk) a #1:3 b; endseguence sequence s30b; (posedge clk) c #2:3 d; endsequence property p30; (posedge clk) first_match(s30a or s30b); endp

22、roperty a30: assert property(p30) ;,首次匹配： 当一个检验有多个匹配时，确保只用第一个匹配，丢弃其他匹配可节省仿真资源,例子：,其它1：使用序列结束点作为同步点”ended”,sequence sl5a; (posedge clk) a #1 b; endsequence sequence sl5b; posedge clk) c #1 d; endsequence property pl5a; sl5a |= sl5b; endproperty property pl5b; sl5a.ended |- #2 sl5b.ended; endproperty

23、al5a: assert property(pl5a); al5b: assert property(pl5b);,说明：检查序列al5a和序列b15b间隔一个周期的延迟,通过使用交叠蕴含和两个周期延长确保了两个序列在结束点同步,之前的定义的序列都是通过简单的连接机制，多个序列以序列的起始点作为同步点 在使用简单序列组织复杂序列时非常有用,# * Error: Assertion error. # Time: 175 ns Started: 75 ns Scope: simple_seq.a15a File: basic.v Line: 98 Expr: c # * Error: Assert

24、ion error. # Time: 225 ns Started: 125 ns Scope: simple_seq.a15b File: basic.v Line: 99 Expr: s15b.ended,其它2：多时钟断言,sequence s_multiple_clocks; (posedge clk1) a #1 (posedge clk2) b; endsequence 说明：在时钟clk1的任何上升沿，信号a为高，接着在时钟的clk2上升沿，信号b为高。 #1 表示检验时间移到时钟clk2的最近上升沿，且允许使用#1延迟构造,例子：,可以使用非交叠运算符，禁止使用交叠运算符 因为

25、交叠运算符的先行算子的结束和后续算子的开始是重叠的，可能引起竞争 property p_multiple_clocks_implied; (posedge clk1) s1 |= (posedge clk2) s2; endproperty,注意：,其它2：检测多时钟序列结束点的“matched”,例子： sequence s_a; (posedge clkl) $rose(a); endsequence sequence s_b; (posedge clk2) $rose(b); endsequence property p_match; (posedge clk2) s_a.matched

26、 |= s_b; endproperty a_match: assert property(p_match);,说明： 如果一个序列定义了多个时钟，构造matched可以用来监测第一个子序列的结束点,其它3：断言中等待属性成功“expect”,例子： initial begin (posedge elk); #2ns cpu_ready = 1b1; expect(posedge clk) #1:16 memory_ready = Ibl) $display(Hand shake successfuln); else begin $display(Hand shake failed: exit

27、ingn) $finish(); end end,说明： 与wait类似，等待属性成功检验，expect后语句作为阻塞语句来执行,其它4：断言中等待属性成功“expect”,例子： initial begin (posedge elk); #2ns cpu_ready = 1b1; expect(posedge clk) #1:16 memory_ready = Ibl) $display(Hand shake successfuln); else begin $display(Hand shake failed: exitingn) $finish(); end end,说明： 与wait类

28、似，等待属性成功检验，expect后语句作为阻塞语句来执行,其它5：在序列中处理数据,例子1： a #1 (b-1, x = e) #1 (c*2, x = x + 1) 说明：b跳转重复1次时，把e赋值给x，当c连续重复两次后，x增1 例子2： property e; int x; (valid_in,(x = pipe_in) |- #5 (pipe_out1 = (x+1); endproperty 说明：5个固定周期监测pipe_out1是否为pipe_in+1 错误例子3： sequence s4; int x; (a #1 b, (x = data) #1 c) or (d #1

29、(e=x); / illegal endsequence 在同时发生的序列中不能访问并发序列中的赋值,说明：该特性在涉及流水检查时非常有用，后续节拍检查不能使用静态变量，必须保存每次序列检查引用的当前需要的n个节拍之前值，当然可存储一组变量，并用移位来模仿流水节拍，但是如果在更复杂的状态，当流水线的延迟是变量而且是乱序的，那种该结构就会比较复杂，易于出错。所以必须使用局部变量。 格式：sequence_expr := | ( expression_or_dist , sequence_match_item ) boolean_abbrev | ( sequence_expr , sequenc

30、e_match_item ) sequence_abbrev .,expression_or_dist : = expression dist dist_list boolean_abbrev := consecutive_repetition | non_consecutive_repetition | goto_repetition,sequence_abbrev := consecutive_repetition,例子4：OR操作符需要注意的地方，局部变量使用需要同时赋值了 sequence s5; int x,y; (a #1 b, x = data, y = data1 #1 c)

31、or (d #1 true, x = data #0 (e=x) #1 (y=data2); / illegal since y is not in the intersection，y没有同时赋值 endsequence sequence s6; int x,y; (a #1 b, x = data, y = data1 #1 c) or (d #1 true, x = data #0 (e=x) #1 (x=data2); / legal since x is in the intersection，x都同时赋值了 endsequence or的每个线程，满足条件后，像独立的线程一样继续,

32、例子5： and and intersect sequence s7; int x,y; (a #1 b, x = data, y = data1 #1 c) and (d #1 true, x = data #0 (e=x) #1 (x=data2); / illegal since x is common to both threads endsequence sequence s8; int x,y; (a #1 b, x = data, y = data1 #1 c) and (d #1 true, x = data #0 (e=x) #1 (y=data2); / legal sin

33、ce y is in the difference endsequence and和intersect每个线程，满足条件后会合成一个线程,其它6：sequence的其他使用方法,sequence abc; (posedge clk) a #1 b #1 c; endsequence program test; initial begin abc $display( Saw a-b-c ); L1 : . end endprogram,sequence abc; (posedge clk) a #1 b #1 c; endsequence sequence de; (negedge clk) d

34、 #2:5 e; endsequence program check; initial begin wait( abc.triggered | de.triggered ); if( abc.triggered ) $display( abc succeeded ); if( de.triggered ) $display( de succeeded ); L2 : . end endprogram,说明： 在事件表达式中根据sequence的成功与否用来控制程序测执行，可以触发事件。 电平敏感序列控制,例子：,Sequence的操作符和方法总结,属性的声明,property_declarat

35、ion := property property_identifier ( list_of_formals ) ; assertion_variable_declaration property_spec ; endproperty : property_identifier ,property_expr := sequence_expr | ( property_expr ) | not property_expr | property_expr or property_expr | property_expr and property_expr | sequence_expr |- pro

36、perty_expr | sequence_expr |= property_expr | if ( expression_or_dist ) property_expr else property_expr | property_instance | clocking_event property_expr,property_spec := clocking_event disable iff ( expression_or_dist ) property_expr,设定检查的起始点-蕴含(implication)算子,交叠蕴含 |- 说明：如果先行算子匹配，那么同一个时钟周期计算后续表达式

37、 (posedge clk) a |- b;,非交叠蕴含|= 如果先行算子匹配，那么下一个时钟周期计算后续表达式 (posedge clk) a |= b;,后续算子带固定延迟的交叠蕴含 (posedge clk) a |- #2 b ; 说明：sequence_expr |= property_expr 等价sequence_expr #1 true |- property_expr,不想检验的属性设置算子disable iff,property p34; posedge clk) disable iff (reset) $rosestart) |= a=2 #1 b=2 #1 !start

38、 endproperty a34: assert propertyp34); 说明：如果reset为高，检验器停止检查，并默认发出一个空成功的信号,格式： disable iff (expression_or_dist) property_expr,例子：,递归属性,说明： 递归属性提供了一种灵活的来编写属性,可用在：在满足复杂触发条件后属性需要保持的地方,property prop_always(p); p and (1b1 |= prop_always(p); endproperty,property p1(s,p); s |= prop_always(p);/p必须在每一个周期保持有效

39、endproperty,property prop_weak_until(p,q); q or (p and (1b1 |= prop_weak_until(p,q); /p必须在每一个周期保持有效 ，但q不需要 endproperty,property check_phase1; s1 |- (phase1_prop and (1b1 |= check_phase2); endproperty property check_phase2; s2 |- (phase2_prop and (1b1 |= check_phase1); endproperty,例子1：,例子2：,互相调用：,递归属

40、性使用的限制,限制：,反向操作符not不能在递归属性中使用 property illegal_recursion_1(p); not prop_always(not p); endproperty,禁止操作符disable iff不能在递归属性中使用 property illegal_recursion_1(p); not prop_always(not p); endproperty,递归属性的的实例化必须在一定数名周期延迟之后 property illegal_recursion_1(p); not prop_always(not p); endproperty,断言声明属性,断言属性介绍

41、： 描述某些属性在DUT（被测设计）上得到证明 如果没有定义else动作，那么报告一个$error动作 目的： 寻求任何可能存在的违反指定的协议的情况 例子： property abc(a,b,c); disable iff (a=2) not clk (b #1 c); endproperty env_prop: assert property (abc(rst,in1,in2) pass_stat else fail_stat;,格式： assert_property_statement:= assert property ( property_spec ) action_block,假定

42、声明属性,assume假设属性的说明： 描述环境的假定行为。仿真过程中，断言的和假定的属性不断被验证，以保证设计或者测试平台不会违反期望的设计行为。 在约束随机化的仿真中，对环境的假设可以作为DUT输入信号的时序约束。,格式： assume_property_statement:= assume property ( property_spec ) ;,例子： 对req信号的要求 property pr1; (posedge clk) !reset_n |- !req; /when reset_n is asserted (0),keep req 0 reset期间req保持无效 endpro

43、perty property pr2; (posedge clk) ack |= !req; / one cycle after ack, req must be de-asserted ack一个周期后，req不能无效 endproperty property pr3; (posedge clk) req |- req*1:$ #0 ack; / hold req asserted until / and including ack asserted req必须保持到ack有效 endproperty,覆盖声明属性,cover覆盖属性介绍： 用于验证功能覆盖率，可以保证设计的边角情况在仿真过

44、程中可以得到验证。工具在仿真结束时会收集评估的信息。当cover成功，通过语句可以定义一个覆盖函数，比如检测序列所有路径。 覆盖 属性：报告尝试次数、成功次数、失败次数、空成功次数 覆盖 序列：报告尝试次数、匹配次数 目的：模拟覆盖系统功能所有可能的情况 例子： module top(input bit clk); logic a,b,c; sequence seq3; (posedge clk) b #1 c; endsequence c1: cover property (seq3); . endmodule,格式： cover_property_statement:= cover pro

45、perty ( property_spec ) statement_or_null,绑定运算符”bind”-设计和SVA相连,设计与SVA连接方法： 在模块的定义中内建或者内联检验器SVA 将检验器与模块、模块的实例或者一个模块多个实例绑定,格式： bind_directive := bind hierarchical_identifier constant_select bind_instantiation ; bind_instantiation := program_instantiation | module_instantiation | interface_instantiatio

46、n,例子： interface range (input clk,enable, input int minval,expr); property crange_en; (posedge clk) enable |- (minval = expr); endproperty range_chk: assert property (crange_en); endinteface bind cr_unit range r1(c_clk,c_en,v_low,(in1 bind module名称 包含属性的接口声明名称 接口实例名称（输入参考信号）,其他,关于时钟的推断： 通常情况下，在属性prop

47、erty的定义中指定时钟，保持序列sequence独立于时钟，可以提高sequence的可重用性。 覆盖率属性 假设属性语句中被实例化或者内嵌，就必须和一个时钟相连，这个时钟可以在属性中指定，也可以从always块或默认时钟块中推断,属性的使用位置： 程序代码外,module top(input bit clk); logic a,b,c; property rule3; (posedge clk) a |- b #1 c; endproperty a1: assert property (rule3); . endmodule,property r4; (posedge mclk)(q !=

48、 d); endproperty always (posedge mclk) begin case (a) 1: begin q = d1; r4p: assert property (r4); end default: q1 = d1; endcase end,嵌入到程序代码中 仿真initial或always块中,控制断言的系统函数,asserton 重新是能检验和执行定义的断言 assertoff 停止验证和执行定义的断言 已经执行的断言不受影响 assertkill 停止验证和执行定义的断言 同样停止已经执行的断言 module可以使用相对或者绝对层次路径 断言使用断言的名称声明 le

49、vels 定义模块受影响的层次 0代表所有层次,格式： assert_control_task := assert_task ( levels , list_of_modules_or_assertions ) ; assert_task := $asserton | $assertoff | $assertkill,注意的规则1,要使用其他运算符来约束开放的时间间隔#n:$,不好的断言：a14:assert property(clk) a |- #1:$ b) 使用交集限制开放时间： a_length:assert property (posedge clk) y |- 1b1 *20:30 intersect (a #1:$ b #1:$ c) ) else ;,使用蕴含限制开放时间： a_within:assert pr