SystemVerilog Assertion常用操作符总结及案例

前言：在数字电路验证中，常常需要对某一组信号之间的关系做检查，此时就要用到SystemVerilog Assertion。用过能掌握SVA的一些语法，将大大减小了check的代码量。针对信号持续重复的情况，SVA提供了三种重复操作符：Consecutive repetition（持续性重复），go to repetition(跟随重复操作）和non-consecutive repetition（非连续重复操作）。本文将分别介绍这三种操作符的含义及使用方法。

一、持续重复操作（Consecutive repetition）

1.1 信号的重复

原语： signal or sequence [*n] 其中n为重复的次数
含义：持续性重复允许指定x信号或序列持续性匹配指定周期数，重复周期之间默认有一时钟周期的间隔。

(a##1b)[*3]; //等价于 a##1b##1a##1b##1a##1b

示例（1）信号的重复：start上升沿两个时钟周期后，a持续为高3个时钟周期，再经过两个时钟周期后，stop拉高1个时钟周期

property p21;@(posedge clk);$rose(start)|->##2 (a[*3]) ##2 stop ##1 !stop;
endpropertya21: assert property(p21) else $error();

1.2 带有延迟窗的重复

property p23;@(posedge clk) $rose |-> ##2 ((a##[1:4]b)[*3]) ##2 stop;
endpropertya23: assert property(p23) else $error();
//(a##[1:4]b)[*3]等价于：
//((a##1b) or (a##2 b) or (a##3 b) or (a##4b))##1
//((a##1b) or (a##2 b) or (a##3 b) or (a##4b))##1
//((a##1b) or (a##2 b) or (a##3 b) or (a##4b))

1.3 带有不确定性的持续性重复

含义：持续性重复可以指定秩序性重复的最小和最大次数，信号持续性重复次数在这个范围内都匹配正确。其重复次数上限可以设为$表示无穷.
示例：a[*1:5]等价于a or (a##1a) or (a##1 a ##1 a) or (a##1 a##1 a##1 a )or (a##1 a##1 a##1 a##1 a)

property p24;@(posedge clk)$rose(start) |-> ##2 (a[*1:$]) ##1 stop;
endpropertya24: assert property(p24) else $error();

二、跟随重复操作（go to repetition）

2.1 不要求信号持续重复，可以是间断性的，但要求最后一次匹配必须在序列匹配的最后一个时钟周期。

原语：Sigbnal [->n]
含义：Start ##1 a[->3] ##1 stop; //要求a重复三次且必须最后一次出现紧接着stop信号。
示例：p25要求a最后一次出现必须紧接着stop信号。

property p25;@(posedge clk) $rose(start) |->##2 (a[->3]) ##1 stop;
endpropertya25:assert property(p25) else $error();

三、非连续重复操作（non-consecutive repetition）

3.1 非持续性重复操作不要求信号连续重复，也不要求信号最后一次匹配必须在序列的最后一个时钟周期。

原语：Signal [=n]
示例：p26中序列要求检测到start上升沿后两个时钟周期后，a应重复3次，但不要求持续重复，随后再过一个时钟周期，stop拉高一个时钟周期。

property p26;@(posedge clk) $rose(start) |->##2 (a[=3]) ##1 stop ##1 !stop;
endpropertya26:assert property(p26) else $error();

注意，start上升沿后两个时钟周期后不要求a立即为高，只需要确保在start上升沿于stop拉高之间有三个a高电平即可，跟随重复操作类似。
案例：check如下sequence：在信号a为高期间，信号b会出现1个posedge，但是信号b出现posedge时，信号a不一定为高电平

property b_posedge();@(posedge clk_ck) disable iff(~rst_n)$rose(a) |-> ($rose(b)[1]) ##1 $fell(a);
endproperty

3.2 区别与联系

[->n]只有给操作符后边跟其他表达式才可以看出两者的区别。
满足[->n]必定满足[=n]，满足[*n]必定满足[->n]和[=n]。

四、其他操作符

4.1 同步操作符intersect

含义：操作符intersect为and操作符特例，它要求两个序列同时开始，同时结束。换句话说，就是要求两个序列的长度必须相等。
示例：p28相当于要求s28a和s28b要有相同的长度序列。

sequence s28a;@(posedge clk) a##[1:2] b;
endsequencesequence s28b;@(posedge clk) c##[2:3] d;
endsequenceproperty p28;@(posedge clk) s28a intersect s28b;
endpropertya28:assert property(p28) else $error();

应用：intersect也可用于控制序列的长度，用于限定那些未设定窗口上限的序列定义检测时长
示例：p35中由于intersect的使用，序列应在三至五个时钟周期内检查完毕，否则断言失败。

property p35;@(posedge clk) 1[*3:5] intersect(a##[1:$] b ##[1:$] c));
endpropertya35:assert property(p35) else $error();

4.2 first_match操作

含义：针对带有时序窗口的序列，同一起始点可能有多个匹配到的序列，fisrt_match用于确保只用第一次匹配成功的序列而丢弃其他匹配的序列，用于针对同一个校验具有多个匹配的情况。
示例：对于p30来讲，对于每个起始点都有5中可能匹配的序列，first_match在得到一个成功匹配的点后，其他情况将不会再考虑匹配。

sequence s30a;@(posedge clk) a##[1:3] b;
endsequencesequence s30b;@(posedge clk) c##[2:3]d;
endsequenceproperty p30;@(posedge clk) first_match(s30a or s30b);
endporpertya32:assert property(p30) else $error();

4.3 throughout操作符

含义：throughout操作符用于保证某些条件在整个序列的验证过程中一直为真。
原语：（expression）throughout （sequence definition）
在整个sequence definition验证期间，expression表达式必须一直保持为真。
即使验证序列匹配成功但表达式不为真，也会导致整个验证序列的验证失败。
示例：p31要求在序列检查期间，start信号必须保持为低电平

property p31;@(posedge clk)$fell(start) |-> (!start) throughout (##1 (!a&&!b) ##1 (c[->3]) ##1 (a&&b));
endpropertya31:assert property(p31) else $error();

4.4 within操作符

原语：seq1 within seq2
含义：with原语规定seq1在seq2的开始到结束范围内发生，即seq2的开始匹配点必须不晚于seq1的开始匹配点，seq2的匹配结束点必须不晚于seq1的结束匹配点。

sequence s32a;@(posedge clk)((!a&&!b) ##1 (c[->3]) ##1 (a##b));
endsequencesequence s32b;@(posedge clk)$fell(start) ##[5:10] $rose(start);
endsequencesequence s32;@(posedge clk) s32a within s32b;
endsequenceproperty p32;@(posedge clk) $fell(start)|->s32;
endpropertya32:assert property(p32) else $error();

4.5 matched

任何时候如果一个序列定义了多个时钟，构造“matched”可以用来监测第一
个子序列的结束点。

sequence s_a; @(posedge clk1) $rose(a);
endsequence sequence s_b; @(posedge clk2) $rose(b);
endsequence property p_match; @(posedge clk2) s_a.matched |=> s_b;
endproperty a_match： assert property(p_match);

五、if/else结构使用

SVA也允许在属性property中使用if/else结构
示例：a取不同值时，进行不同的check

property p_if_else;@(posedge clk) ($fell(start) ##1 (a||b)) |->if(a)(c[->2] ##1 e);else(d[->2] ##1 f);
endpropertya_if_else:assert: property(p_if_else) else $error();

六、expect操作符

含义：expect操作符类似于verilog中的wait。
作用：expect用于等待一个成功检测的property，并带有阻塞作用。
原语：expect的原语结构非常类似于assert，并允许带有成功与失败情况下的响应块儿（else ...）。
示例：当cpu_ready被置位后，expect期待在1至16个时钟周期内memory_ready被置位。若memory_ready如期被置位，执行for循环，否则报错并退出。

initial begin@(posedge clk);#2ns cpu_ready=1'b1;expect(@(posedge clk) ##[1:16] memory_ready =='b1)$dispaly("Hand shake successful\n");else begin$display("Hand shake failed:exiting");$finish();endfor(i=0;i<64;i++) begin...end
end

七、局部变量的使用

SVA允许在property和sequence中声明局部变量。局部变量在使用时紧跟子序列，用逗号隔开。
当子序列成功匹配时，变量赋值被执行。每次序列执行时，变量均会创建一个副本。
示例：p_local_var1中$rose(enable1)匹配成功才会对lvar1赋值。

property p_local_var1;int lvar1;@(posedge clk)($rose(enable1),lvar1=a) |-> ##4 （aa==(lvar1*lvar1*lvar1)）;
endpropertya_local_var1: assert property(p_local_var1) else $error();

八、逻辑操作符

8.1 and

逻辑操作符and用于组合两个序列，当所有的序列都成功匹配后才通过检测。所有的序列在同一时间开始但可以在不同时间结束。

sequence s27a;a##[1：2] b;
endsequecesequence s27b;c##[2:3] d;
endsequenceproperty p27;@(posedge clk) s27a and s27b;
endpropertya27:assert property(p27) else $error();

8.2 or

逻辑操作符or当序列中的其中一个验证成功后即匹配成功。

sequence s29a;@(posedge clk) a##[1:2] b;
endsequencesequence s29b;@（posedge clk）c##[2:3]d;
endsequenceproperty p29;@(posedge clk) s29a or s29b;
endpropertya29: assert property(p29) else $error();

[SVA]SystemVerilog Assertion常用操作符总结及案例相关推荐

[SVA]SystemVerilog Assertion(SVA)編寫經驗
SystemVerilog Assertion(SVA)編寫經驗 1.断言的目的传统的验证方法是通过加激励,观察输出.这种方法对案例的依赖严重,案例设计不好,问题不便于暴露.而断言是伴随RTL代码的 ...
Python零基础入门（3）——常用操作符介绍
1.总结python[版本3.6]中的常用操作符操作符(常用的操作符)分为: 算术操作符:[+][-][*][/][%][**][//] 逻辑(布尔)操作符 :[and] [or][not] 比较( ...
AI之NLP：自然语言处理技术简介(是什么/学什么/怎么用)、常用算法、经典案例之详细攻略(建议收藏)
AI之NLP:自然语言处理技术简介(是什么/学什么/怎么用).常用算法.经典案例之详细攻略(建议收藏) 目录 NLP是什么? 1.NLP前置技术解析 2.python中NLP技术相关库 3.NLP案例 ...
Py之re：re正则表达式库的简介、常用函数、经典案例之详细攻略
Py之re:re正则表达式库的简介.常用函数.经典案例之详细攻略目录 re正则表达式库的简介 1.正则表达式元字符表集合--正则表达式的pattern re正则表达式库的常用函数 1.re.comp ...
Matlab：Matlab中常用的函数、案例详细攻略
Matlab:Matlab中常用的函数.案例详细攻略目录常用函数 1.与文件相关 2.MATLAB GUI不同控件函数间变量传递方法常用函数 Matlab中的bwmorph函数解释 bwmorp ...
可视化篇（二）———使用matplotlib绘制常用3D图形及案例
可视化篇(二)---使用matplotlib绘制常用3D图形及案例摘要 (一)添加matplotlib 3D模块 (二)3d图中绘制曲线 (三)3d图中绘制散点图 (四)3d图中绘制线框图 (五)3 ...
RabbitMQ常用操作命令和入门案例（一对一的简单模式）
RabbitMQ常用操作命令和入门案例(一对一的简单模式) 一.RabbitMQ常用操作命令常见命令列表: # 前台启动Erlang VM和RabbitMQrabbitmq-server # 后台启 ...
二级VB培训笔记06：窗体与常用控件综合案例【个人信息注册】
二级VB培训笔记06:窗体与常用控件综合案例[个人信息注册] 一.常用控件属性与方法思维导图二.综合案例--个人信息注册 1.创建工程,修改名称为"个人信息注册",窗体名称设置为 ...
VHDL常用操作符介绍
1.1 VHDL常用操作符介绍 1.1.1 本节目录 1)本节目录: 2)本节引言: 3)FPGA简介: 4)VHDL常用操作符介绍: 5)结束语. 1.1.2 本节引言 "不积跬步,无以至 ...

[SVA]SystemVerilog Assertion常用操作符总结及案例