立即断言（immediate assertion）：

并行断言（concurrent assertion）：

assertion，property，sequence介绍

基本操作符号

局部变量

调用方法

系统函数和方法

断言可以用来完成：

1、检查设计的内容。

2、提高设计的可视度和调试能力。

3、检查设计特性在验证中是否被覆盖。

4、可读性好，因此也可以用来服务与设计文档。

5、用来检查算法模型的断言在形式验证(formal verification)中可以穷尽计算，找出可能的违例(violation)。

6、可以自由打开或者关闭。

7、一小部分子集甚至可以用来综合或者移植到emulation中，用来完成跨平台移植。

断言覆盖率

仿真工具可以报告断言覆盖率，来指示哪些断言没有被触发，帮助检查是否验证计划捕捉到了多有需要的覆盖率，断言覆盖率和功能覆盖率可以共同量化验证进度。在Verilog中不支持断言，因此需要写过程语句来做替代。

断言分类

立即断言（immediate assertion）：

非时序的、执行时如同过程语句、可以在initial/always过程块或者task/function中使用。

[name:] assert(expression)[pass_statement] [else fail_statement];

立即断言可以结合$fatal$error$warning$info给出不同严重级别的消息提示。

并行断言（concurrent assertion）：

时序性的、关键词property用来区分立即断言和并行断言、之所以称为并行，是因为他们与设计模块一同并行执行。

base_rule：assert property（cont_prop(rst,in1,in2)） pass_stat else fail_stat;

并行断言只会在时钟边沿激活，变量的值使采样到的值。

assertion，property，sequence介绍

assertion可以包含一个property，assertion也可以清晰地独立声明property，在property内部可以有条件地关闭。

property块可以直接包含sequence，复杂的property也可以独立声明多个sequence。

sequence是用来表示在一个或者多个时钟周期内的时序描述，是property的基本构建模块，并经过组合来描述复杂的功能属性。

sequence用来提供下列的场景描述：第一个时钟周期，第一个表达式成立的，接下来在若干时钟周期后，第二个表达式也成立，一次类推，在接下来的若干时钟周期，后续的表达式也成立。

sequence可以在module、interface、program、clocking块和package中声明。

sequence也可以提供形式参数，用来提高复用性。

蕴含(implication)操作符用来表示，如果property中左边的先行算子(antecedent)成立，那么property右边的后续算子(consequent)才会被计算。如果先行算子不成功，那么整个属性就默认得被认为成功，这叫做“空成功”(vacuous success)。蕴含结构只能用在属性定义中，不能在序列中使用。

蕴含可以分为两类：交叠蕴含(overlapped implication)和非交叠蕴含(non-overlapped implication)。

|->操作符号是交叠交错符号，如果条件满足，则评估其后续算子序列，如果条件不满足，则表现为空成功，不执行后续算子。

|=>操作符号是非交叠交错符号，如果条件满足，则评估其后续算子序列，如果条件不满足，则表现为空成功，不执行后续算子

基本操作符号

##用来表示周期延迟符号，例如##n表示在n个时钟周期后，##0表示在当前周期，即交叠周期。

##[min:max]表示在一个范围内的时钟周期延迟。min、max必须是非负数,序列会在从min到max时间窗口中最早的时间来匹配。

$用来表示无穷大的周期(在仿真结束前)，但是一般我们不建议这么做，因为它会增大仿真评估序列的负担。

事件也可以通过[*n]操作符号来表示重复。n须为非负数，其不能为$。

类似地,也可以使用[*m:n]来表示一定范围内的重复事件。

[=m]用来表示一个事件的连续性，需要重复发生m次，但是并不需要在连续周期内发生。

b[=3]表示b必须在3个周期内为1，但是并不需要是连续的3个周期。

例如，执行了一次burst read操作，期望读的数据和ack信号在接下来的4个周期内返回，但又不需要连续的4个周期，即可以使用[=4]来表示。

类似地，[=m:n]用来表示从最小m到最大n的重复发生的非连续周期次数。

a[*0]用来表示没有在任何正数时钟周期内有效

and用来表示两个序列需要保持匹配。

用法:SEQ1 and SEQ2。

下列情形将满足此操作符:在从同一个起始点开始后，seq1和seq2均满足。满足的时刻发生在两个序列都满足的周期，即稍晚序列的满足时刻。两个序列的满足时间可以不同。

如果操作符两边的序列都是用来衡量采样信号而非事件时序，那么则要求在相同周期内，and左右两边的序列都应该满足条件。

intersect操作符号

与and操作符类似，只是需要两边的序列时序在同一时钟周期内匹配。

(te1##[1:5] te2) intersect (te3##2 te4 ##2 te5)

or操作符号

OR用来表示两个序列至少需要有一个满足。

用法: SEQ1 or SEQ2

下列情形将满足此操作符:

. seq1和seq2都从同一个时刻被触发。

·最终满足seq1或者满足seq2。

·每一个序列的结束时间可以不同，结束时间以序列满足的最后一个序列时间为准。

first_match操作符号

first_match用来从多次满足的序列中选择第一次满足时刻，从而放弃其它满足的时刻。

t1序列可以用来匹配te1##2te2, te1##3te2, te1##4te2或者te1##5te2。

此序列则用来选择第一次匹配的时刻。

对于上述的几种可能满足的sequence，ts2只会选择第一个满足上述sequence的时刻点。

throughout操作符号

可以用来检查一个信号或者一个表达式在贯穿(throughout)一个序列时是否满足要求。

用法:Sig1/Exp1 throughout Seq。

例如，在burst模式信号拉低以后的2个周期时，irdy/trdy也应该在连续7个周期内保持为低，同时burst模式信号也应该在这一连续周期内保持为低。

within操作符号

可以用来检查一个序列与另外一个序列在部分周期长度上的重叠。

用法:SEQ1 within SEQ2

如果当seq1满足在seq2的一部分连续时钟周期内成立，seq1 withinseq2成立。

例如，trdy需要在irday下拉的1个周期后保持7个周期为低，同时irday也将保持8个周期为低，以下序列会在第11个时钟周期满足。

if操作符号

我们可以在sequence中使用if..else。

例如，当master_req为高时，下一个周期，reql或者req2应该为高，如果req1为高，则下一个周期ack1为高，如果req2为高，则下一个周期ack2为高。

end操作符号

用法:SEQ.ended

在某一时刻，序列如果及时抵达终点)那么条件满足。例如，在inst为高的下一个周期，列ei应该结束或者已经结束。

在c拉起的下一个周期，a拉低b拉高的序列也应该结束。

局部变量

局部变量可以在sequence或者property中使用。这些变量会伴随着sequence、property动态创建。每一个sequence实例都会有它自己的变量拷贝。

例如，在cache rdDone拉高后，读出的rdData会在2个周期后，在其基础上加1，并作为wrData写入。

例如，如果read拉高，伴随readld，则下一次read必须在这一次read对应的readAck返回之后，才可以发起。

需要先记录上一次read的readld，继而在接下来的周期，检查没有相同readld的read发起，直到对应readld的上一次read的readAck拉起，并且readAckld与之相同。

调用方法

在序列匹配时，可以调用task，void function和系统函数。

例如，可以在s1序列末尾，分别打印出e和f变量被采样时的数值。

访问采样方法

一些系统函数可以用来访问指定类型的变量采样:

·用来访问当前周期采样值。

·用来访问上一个采样周期值。

·用来检测采样变量的变化。

$rose(expression[, clocking_event])和$fell(expression[,clocking_event])用来表示与上一个采样周期相比，变量最低位是否跳变为1或者0，满足条件返回1，否则返回0。

clocking_event在sequence中不需要单独提供，因为sequence中一般会指定采样时钟。

例如，在Req拉起的2个周期以后，Ack也应该拉高。

例如，在write_en拉低后(表征发起写访问),write_data的数据内容不应该为X。

$stable(expression[, clocking_event])，用来表示在连续两个采样周期内，表达式的值保持不变，如果满足，返回1，否则，返回0。

例如，在rd_en为高时，寄存器的值应该保持不变。

$past[expr[, num_cycles][, gating_expr][, clocking_event])用来访问在过去若干采样周期前的数值。

默认情况下，num_cycles=1，即采样1个周期前的数值。

例如,在ack拉高时的前两个周期,req信号应该为高。

例如，如果当前状态是CACHE_RED，那么上一个状态不应该是CACHE_MlSS(如果cache丢失，那么无法从中读取数据)。

$rose/$falll/$stable也可以在过程块语句和连续赋值中使用。

系统函数和方法

类似于之前的访问采样的方法，我们还可以使用其它一些系统函数和方法，在sequence/property/assertion中使用:

$countbits

$onehot

$isunknown

$countones

这些系统函数也可以用在一般的过程语句块和赋值语句中。

$countbits(expression, control_bit)用来计算expression中匹配control_bit数值的位数。

$countones(expression)与$countbits(expression，‘1)一致,即计算expression中为1的位数。

$onehot(expression)与$countbits(expression，‘1)==1—致，即检查expression中是否有且只有1位为1。

$isunknown(expression)与$countbits(expression，‘x,‘z)!=0一致，即检查expression中是否有x或者z。

level=0，表示当前模块或者层次下的所有assertion。

level=n，表示当前模块或者层次下n层范围中的assertion。

assertion_identifier表示property的名字或者assertion的label。

例如，在reset阶段停止所有的assertion，并且在其复位之后，使能所有的assertion。

时钟声明

一般对于sequence或者property，默认情况下，在使用同一个时钟用来对数据做采样，但是也不排除多个时钟的采样情况。

如果一个sequence或者property需要声明多个时钟用来做数据采样，可以使用##1结合第二个时钟沿采样。

我们只能使用##1来表示与第一个时钟(clk1)沿紧密相连的下一个时钟(clk2)沿。

sequence操作符号例如and、or、intersect等无法被使用在多时钟sequence。

property中的and、or、not则可以用在多时钟的pryperty声明中，因为它们进代表逻辑运算，并不参与sequence之间的时序关系。

在时钟块中，也可以继承时钟块的时钟。

由此，断言的时钟由以下条件的优先级逐级判定:

显式声明断言时钟。

继承断言所嵌入环境的时钟。

继承默认的时钟。

对于并行断言，其必须具备时钟，即满足上述时钟条件之一。

对于多时钟的断言，必须显式声明时钟，无法继承或者使用默认时钟。

如果是多时钟断言，也无法嵌套入由时钟驱动的过程块语句。

多时钟断言,也无法嵌套入时钟块。

expect语句

之前的assert、assume和cover都是非阻塞的方式，即它们本身并不会阻塞后续的语句，然而，expect则是一种阻塞的property使用方式。

expect的语法同assert一致,不过它会等待property执行通过，才会执行后续的语句。

简单来看，可以使用wait语句的地方，即可以使用expect语句。

同assert语句的调用方式类似，它也可以使用在function和task中，同时也可以引用静态变量或者动态变量。

SVA——断言属性之序列（sequence与property的用法）_disable iff_SD.ZHAI的博客-CSDN博客

SystemVerilog Assertion(SVA)学习笔记（一）：知识点总结 - 知乎 (zhihu.com)

断言(Assertion)相关推荐

SQL入门(3):定义约束/断言assertion/触发器trigger
本文介绍数据库的完整性完整性控制程序: 指定规则,检查规则 (规则就是约束条件) 动态约束 intergrity constraint::=(O,P,A,R) O : 数据集合, 约束的对象 ?: ...
java断言——Assertion
[0]README 0.1) 本文描述+源代码均转自 core java volume 1, 旨在理解 java断言--Assertion 的相关知识: [1]使用断言 1.1)断言机制: 允许在测 ...
java断言是什么_Java断言(Assertion)
断言(Assertion)是Java中一条语句,包含一个布尔表达式,当该布尔值为真,程序则被认为是正确的:当布尔值为假,则系统会抛出错误. 断言默认禁用的,在开发时候可开启功能,有利于纠正错误,增加可 ...
断言Assertion
什么是断言在程序设计中,断言(assertion)是一种放在程序中的一阶逻辑(如一个结果为真或是假的逻辑判断式),目的是为了标示与验证程序开发者预期的结果 -当程序运行到断言的位置时,对应的断言应该 ...
断言(Assertion)需要注意的一个地方
因为断言只在debug构建中有效,所以它是中关重要的去避免运行任何代码或调用任何方法在断言条件中,而这些代码或方法会影响程序的状态. 否则程序的行为将在debug和release构建中变得不一致,这显 ...
systemVerilog Assertion （SVA）断言语法
转载自:http://blog.sina.com.cn/s/blog_4c270c730101f6mw.html 作者:白栎旸断言assertion被放在verilog设计中,方便在仿真时查看异常情 ...
Java中的断言(assert)
为什么80%的码农都做不了架构师?>>> 一.语法形式: Java2在1.4中新增了一个关键字:assert.在程序开发过程中使用它创建一个断言(assertion), ...
java高级断言_Java之断言
转自博客:http://blog.csdn.net/tanga842428/article/details/52463694 一.语法形式 Java在1.4中新增了一个关键字:assert.在程序开发 ...
断言、触发器、存储过程
断言 assertion 设置每一门课程最多有60人选修 create assertion a check (60 >= all ( select count(*) from sc group ...

断言(Assertion)

立即断言（immediate assertion）：

并行断言（concurrent assertion）：

assertion，property，sequence介绍

基本操作符号

局部变量

调用方法

系统函数和方法

断言(Assertion)相关推荐

最新文章

热门文章