SystemVerilog Assertion断言学习

1、何为断言，有何作用

断言是一种描述性语言，用于描述设计的属性(property)，可以完美地描述时序相关的状况。如果允许的设计属性不符合我们的期望，则断言失败；如果被禁止的设计属性发生，则断言失败。属性可以从设计的功能描述中推知，并被转换为断言(SVA)。断言通常又被成为监视器或检验器。

断言的评估和执行包括以下三个阶段：

预备(Preponed)：在这个阶段，采样断言变量，而且信号(net)或变量(variable)的状态不能改变。这样确保在时隙开始的时候采样到最稳定的值；

观察(Observed)：在这个阶段，对所有的属性表达式求值；

响应(Reactive)：在这个阶段，调度评估属性成功或失败的代码。

2、断言与设计连接

有两种方法可以将SVA检验器连接到设计当中：

1）在模块(module)定义中内建或者内联检验器；

2）将检验器与模块、模块的实例或者一个模块的多个实例绑定。

第一种方法直接在module中添加断言代码，不需要多加赘述。第二种方法采用bind来实现，将单独的检验器(SVA)模块挂接在设计中任何的模块(module)或实例(instance)。绑定语法如下所示：

bind <module_name orinstance_name> <checker name> <checker instance name> <design signals>

其中checker name为检验器，采用独立的module实现，在module中把断言行为assert描述出来，这样就可以重复利用，增强重用性。

3、断言分类

SystemVerilog语言中定义了两种断言：并发断言和即时断言(立即断言)。

1）并发断言

基于时钟周期；
在时钟边缘根据调用的变量的采样值计算测试表达式；
变量的采样在预备阶段完成，而表达式的计算在调度器的观察阶段完成；
可以被放到过程块(procedural block)、模块(module)、接口(interface)，或者一个程序(program)的定义中；
可以在静态(形式的)验证和动态验证(模拟)工具中使用。
如： a_cc: assert property (@(posedge clk) not (a && b));

2）即时断言

基于模拟事件的语义；
测试表达式的求值就像在过程块中的其它Verilog的表达式一样。它们的本质不是时序相关的，而且立即被求值；
必须放在过程块的定义中；
只能用于动态模拟。

    如：

 always_comb
 begin
   a_ia: asser (a && b);
 end

即时断言a_ia被写成一个过程块的一部分，它遵循和信号a、b相同事件调度。当信号a或者信号b发生变化时，always块被执行。

区别即时断言和并发断言的关键词是“property”。

4、断言组成

断言的语法结构主要分五个部分：

第一层：布尔表达式，这个和Verilog中没有差别；

第二层：序列(sequence)，其中包含一些新的操作符，如##时隙延迟、重复操作符、序列操作符等，序列是一个封装格式，采用序列封装后可以在不同地方使用，一个序列会被评估为真或者假；

第三层：属性(property)，这是重要的封装方式，其中最重要的特点是属性内部可以定义蕴涵操作符(|->、|=>)；

第四层：断言指示层(assert)，也就是采用assert对特定属性或者序列做行为检查，或者采用cover做统计等；

第五层：封装(module、program、interface)，断言的最后封装，只有通过最后封装成一个单元的断言才可以在不同的地方重用，就如同一个可以例化模块或者类，通常这一层可以通过module或者program、interface来封装。

5、断言常用操作符

n：表示延时n个时钟周期；

[m:n]：可以指定窗口，假如和##一起用，如##[1:5]，表示后续事件在1~5个周期的这个窗口内出现都可以判定为真，等效于：##1 || ##2 || ##3 || ##4 || ##5，只有其中一种情况为真，则##[1:5]为真；

|->：交叠蕴涵，如果先行算子匹配，在同一个时钟周期计算后续算子表达式。蕴涵等效于一个if-then结构，蕴涵的左边叫作“先行算子”(antecedent)，右边叫作"后续算子"(consequent)。先行算子是约束条件。当先行算子成功时，后续算子才会被计算。如果先行算子不成功，那么整个属性就默认地被认为成功，这叫作“空成功”(vacuous success)。蕴涵结构只能被用在属性定义中，不能在序列中使用；

|=>：非交叠蕴涵，如果先行算子匹配，那么在下一个时钟周期计算后续算子表达式。后续算子表达式的计算总是有一个时钟周期的延迟，等于|->##1；

边沿检查函数：$rose(boolean expression or signal_name)：当信号/表达式的最低位变成1时返回真；$fell(boolean expression or signal_name)：当信号/表达式的最低位变成0时返回真；$stable(boolean expression or signal_name)：当表达式不发生变化时返回真。

参考文献：

SystemVerilog assertions应用指南