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应用指南

更多相关阅读

Bash shell语言学习
Makefile文件

作者:谷公子
首发博客:https://blog.csdn.net/W1Z1Q/article/details/101638207
更多IC设计相关的文章请关注IC设计极术专栏,每日更新。

发表评论

邮箱地址不会被公开。 必填项已用*标注

相关