SV -- Assertions 断言
SV – Assertions 断言
文章目录
- SV -- Assertions 断言
- 1.简介
- 1.1 立即断言
- 2.SVA (system verilog assertion)
- 2.1 Sequence
- 2.2 Property
- 2.2.1 implication
- 2.2.2 repetition 重复操作
- 2.2.3 go to repetition 跟随重复
- 2.2.4 Nonconsecutive repetition 非连续重复
- 2.2.5 throughout
- 2.2.6 within
- 2.3 SVA 方法
- 2.3.1 $rose
- 2.3.2 $fell
- 2.3.3 $stable
- 2.3.4 $past
- 2.3.5 内置系统方法
- 2.3.6 disable iff
- 2.3.7 ended
- 2.4 Variable Delay
1.简介
断言assertion被放在verilog设计中,方便在仿真时查看异常情况。当异常出现时,断言会报警。一般在数字电路设计中都要加入断言,断言占整个设计的比例应不少于30%。
断言的作用:
- 检查特定条件或事件序列的出现情况。
- 提供功能覆盖
断言的种类:
- 立即断言 Immediate Assertions
- 并发断言 Concurrent Assertions
1.1 立即断言
立即断言检查当前仿真时间的条件,相当于 if else , 需要放在过程块中。
语法
label: assert(expression) action_block;
其中:
- action block 操作块在断言表达式的求值之后立即执行
- 操作块指定在断言成功或失败时采取什么操作
action_block:
pass_statement; else fail_statement;
由于断言表达式中所断言的条件必须为真,因此断言的失败将具有与之相关的“严重”程度。默认情况下,断言失败的严重程度是一个error。
还有其他可选的fail statement:
(严重等级依次递减)
- $fatal : a run-time fatal.
- $error : a run-time error.
- $warning : a run-time warning
- $info :information.
例如:
//With Pass and Fail statement; Fail verbosity fatal;
assert(expression) $display(“expression evaluates to true”); else $fatal(“expression evaluates to false”);
立即断言案例:
module asertion_ex;bit clk,a,b;//clock generationalways #5 clk = ~clk;//generating 'a'initial begina=1;b=1;#15 b=0;#10 b=1;a=0;#20 a=1;#10;$finish;end//Immediate assertionalways @(posedge clk) assert (a && b);endmodule
output :
ncsim: *E,ASRTST (./testbench.sv,23): (time 15 NS) Assertion asertion_ex.__assert_1 has failed
ncsim: *E,ASRTST (./testbench.sv,23): (time 25 NS) Assertion asertion_ex.__assert_1 has failed
ncsim: *E,ASRTST (./testbench.sv,23): (time 35 NS) Assertion asertion_ex.__assert_1 has failed
Simulation complete via $finish(1) at time 55 NS + 0
###1.2 并发断言
并发断言检查跨越多个时钟周期的事件序列。
- 并发断言仅在有时钟周期的情况下出现
- 测试表达式是基于所涉及变量的采样值在时钟边缘进行计算的
- 它可以放在过程块、模块、接口或程序定义中
- 区别并发断言和立即断言的关键字是property
c_assert: assert property(@(posedge clk) not(a && b));
2.SVA (system verilog assertion)
下图显示了创建SVA检查器的步骤:
- Boolean expressions: 基本的逻辑信号组成的布尔表达式
- Sequence: 布尔表达式事件,在一段时间内计算涉及单个/多个时钟周期的值。SVA提供一个名为“sequence”的关键字来表示这些事件。
- 语法:
sequence name_of_sequence;endsequence
- Property : 一般用来定义一个有时间观念的断言,它会常常调用sequence,一些时序操作如“|->”只能用于property, 而不能用于立即断言。
2.1 Sequence
Sequence 可以带参数,例如sequence seq_lib (a, b),可以在其他sequence中例化:seq_lib(req1,req2);
Example:
sequence seq_1;@(posedge clk) a==1;
endsequence
在SVA中,时钟周期延迟用“##”符号表示。例如,##2表示2个时钟周期
sequence seq;@(posedge clk) a ##2 b;
endsequence
上面代码表示在上升沿,检测a是否为1,如果否,则断言失败,否则,查看2个周期后的b是否为1,如果是,则断言通过。
通常,在sequence中不定义时钟语句,而在property中定义:
sequence seq;a ##2 b;
endsequenceproperty p;@(posedge clk) seq;
endproperty
a_1 : assert property(p);
2.2 Property
property也可以像sequence一样定义参数,同时也可以在property内部定义变量,如: int a;
另外,如果这么写 a_3: assert property(@(posedge clk) p) ,如果p中也有clk语句,则不允许。
not的写法:
sequence seq;@(posedge clk) a ##2 b;
endsequenceproperty p;not seq;
endproperty
a_1: assert property(p);
not表示断言的内容不发生,也就是要么a不为1,要么a为1但延时2以后b还不为1.
2.2.1 implication
implication只能在property中使用,它的作用如下:
sequence seq;@(posedge clk) a ##2 b;
endsequence
在上面这段断言中,表示如果在上升沿a为1,之后2个延时后b也为1,那么断言成功,而如果a在上升沿就不是1,那么每个这样的情况都会报error,这可能不是我们希望的。我们可能只想要在a为高之后才进行断言。
于是就有了implication(蕴含,不知道是不是这么翻译)。 它的逻辑类似于下面的代码:
if a then b; else succeed;
因此,一旦 a 发生,b必须发生,断言才成功。如果a没发生,走else,同样成功而不会报错。
implication分为两种:
- Overlapped implication (|->) 交叠蕴含
- Non-overlapped implication(|=>) 非交叠蕴含
Overlapped implication (|->):
表示左边的条件发生时,立即检查右边的是否发生。
property p;@(posedge clk) a |-> b;
endproperty
a: assert property(p);
上面的代码表示当a为1时,在同一个上升沿检查b是否为1.
Non-overlapped implication(|=>):
与上面不同的是|=>表示左边的条件发生时,在下一个周期检查右边的是否发生。
property p;@(posedge clk) a |=> b;
endproperty
a: assert property(p);
上面的代码表示当a为1时,在下一个上升沿检查b是否为1.
timing windows:
property p;@(posedge clk) a |-> ##[1:4] b;
endproperty
a: assert property(p);
表示在a为高的上升沿后,b需要在1-4个周期内置高。
其中,如果用$代替4:##[1:$]则表示最大时间,也就是直到仿真结束时间。
2.2.2 repetition 重复操作
property p;@(posedge clk) a |-> ##1 b ##1 b ##1 b;
endproperty
a: assert property(p);
这个断言表示 a为高的上升沿后,b需要保持三个周期的高
当然,也可以使用下面的写法:
property p;@(posedge clk) a |-> ##1 b[*3];
endproperty
a: assert property(p);
2.2.3 go to repetition 跟随重复
property p;@(posedge clk) a |-> ##1 b[->3] ##1 c;
endproperty
a: assert property(p);
其中##1 b[->3]表示在a为高的上升沿后,经过一个周期,b在接下来要有三个上升沿为高,而且不一定要连续。但有个要求,就是在##1 c发生之前的上升沿b是刚好完成最后一次匹配
2.2.4 Nonconsecutive repetition 非连续重复
跟上面类似,如果改为:b[=3],就是非连续重复,区别是,不要求b的最后一次匹配发生在c发生之前。也就是b完成了三次匹配后,可以等若干周期c才发生
2.2.5 throughout
蕴含(implication)是目前讨论到的允许定义前提条件的一项技术。例如,要对一个指定的序列进行检验,必须某个前提条件为真。也有这样的情况,要求在检验序列的整个过程中,某个条件必须一直为真。蕴含只能在时钟沿检验前提条件一次,然后就开始检验后续算子部分,因此它不检测先行算子是否一直保持为真。为了保证某些条件在整个序列的验证过程中一直为真,可以使用“throughout”运算符。运算符“throughout”的基本语法如下所示:
(expression)throughout (sequence definition)
示例:
property p31;@(posedge clk) $fell(start) |->(!start) throughout (##1 ( !a && !b ) ##1 ( c[->3] ) ##1 ( a&&b ) );endpropertya31: assert property(p31);
p31检查下列内容:
- 在信号“start”的下降沿开始检查。
- 检查表达式((!a&&!b)##1(c[->3])##1(a&&b))。
- 序列检查在信号“a”和“b”的下降沿与信号“a”和“b”的上升沿之间,信号“c”应该连续或间断地出现3次为高电平。
- 在整个检验过程中,信号“start”保持为低。
2.2.6 within
“within”构造允许在一个序列中定义另一个序列。
seq1 within seq2
这表示seq1在seq2的开始到结束的范围内发生,且序列seq2的开始匹配点必须在seq1的开始匹配点之前发生,序列seq1的结束匹配点必须在seq2的结束匹配点之前结束。
2.3 SVA 方法
2.3.1 $rose
sequence seq_rose;@(posedge clk) $rose(a);
endsequence
当a的最低位从0变为1时(在上升沿),断言成功。否则失败。
2.3.2 $fell
sequence seq_fell;@(posedge clk) $fell(a);
endsequence
与rose相反,断言a的最低位从1变0.
2.3.3 $stable
@(posedge clk) $stable(a);
断言a在clk每个上升沿都保持不变。
2.3.4 $past
property p;@(posedge clk) b |-> ($past(a,2) == 1);
endproperty
a: assert property(p);
提供信号在之前周期的值。例如上面例子断言在上升沿,b为1时,两个周期前的a也为1.
此外,$past还有一个gating变量:
@(posedge clk) b |-> ($past(a,2,c) ==1);
上例中c就是这个变量,该断言判断在给定的正时钟边缘上,如果b为高,那么在此之前的2个周期中,只有当选通信号“c”在时钟的任意正边缘上有效时,a才高。
2.3.5 内置系统方法
a_1: assert property( @(posedge clk) $onehot(state) );
a_2: assert property( @(posedge clk) $onehot0(state) );
a_3: assert property( @(posedge clk) $isunknown(bus) ) ;
a_4: assert property( @(posedge clk) $countones(bus)> 1 );
- $onehot(expression)
检查是否只有一位为高 - $onehot0(expression)
检查是否只有一位或0位为高 - $isunknown(expression)
检查是否有任意比特为 X or Z. - $countones(expression)
计数表达式中为高的比特的个数
2.3.6 disable iff
在某些设计条件下,我们不想继续检查某些条件是否正确。这可以通过使用禁用iff来实现。
property p;@(posedge clk)disable iff (reset) a |-> ##1 b[->3] ##1 c;
endproperty
a: assert property(p);
disable iff后面的条件为停止检查的判断条件。上面在reset为低时会检查a |-> ##1 b[->3] ##1 c,直到reset为高,停止检查
2.3.7 ended
默认情况下,多重sequence的组合是以个sequence的起始时间作为同步标志的,SVA提供ended结构以sequence的结束时间作为序列同步点。ended的用法如下:
sequence s1;@(posedge clk) a##1 b;
endsequence
sequence s2;@(posedge clk) c ##1 d;
endsequence
property p1;
s1|=>s2; //s1的成功匹配点滞后一时钟周期是s2匹配的起点
endproperty
property p2;
s1|=>##1 s2.ended; //s1成功匹配点滞后两个时钟周期是s2成功匹配点,即s1匹配成功则再过两个时钟周期s2必须匹配成功
endproperty
property p3;
s1.ended|=>s2; //s1的成功匹配点滞后一时钟周期是s2匹配的起点
endproperty
property p4;
s1.ended|=> ##1 s2.ended;//s1成功匹配点滞后两个时钟周期是s2成功匹配点,即s1匹配成功则再过两个时钟周期s2必须匹配成功
endproperty
若使用ended,则sequence必须定义时钟。关键字ended存储一个反映在指定时钟处序列是否匹配成功的布尔值。该布尔值尽在同一时钟内有效。
2.4 Variable Delay
直接使用##v_delay会导致编译错误,因为在断言中使用变量是非法的。比如下面的例子:
module asertion_variable_delay;bit clk,a,b;int cfg_delay;always #5 clk = ~clk; //clock generation//generating 'a'initial begincfg_delay = 4;a=1; b = 0;#15 a=0; b = 1;#10 a=1;#10 a=0; b = 1;#10 a=1; b = 0;#10;$finish;end//calling assert propertya_1: assert property(@(posedge clk) a ##cfg_delay b);endmodule
上面的代码编译时会出错。解决方法是:##4 (“废话”,var = Signal),一定要有断言的话我们就写“废话”,例如:data == data等。如果有多个变量要赋值也可以,##4(废话,变量1赋值,变量2赋值…)
例如:
sequence delay_seq(v_delay);int delay;(1,delay=v_delay);
endsequence
SV -- Assertions 断言相关推荐
- SV之Assertions 断言
SVA简介 SVA是systemverilog的一个子集,主要用来验证设计的行为,一条断言是嵌入的一条检查语句,可以在特定条件或事件序列的故障上生成警告或错误:断言一般跟在RTL代码后面,如下: mo ...
- [SV]SystemVerilog 断言(SVA)检查器库(OVL)
SystemVerilog 断言(SVA)检查器库(OVL) 前言:SystemVerilog 断言(SVA)检查器库由如下两部分组成: 由检查器组成的SystemVerilog验证库(SVL),这些 ...
- Junit5系列-Junit5中Assertions断言类
目录 系列导航 简介 案例解析 源码解析 Assertions与AssertNull 系列导航 点击跳转到系列博文目录导航 简介 junit5中的JUnit Jupiter提供了Assertions类 ...
- 单元测试框架NUnit 之 assertions 断言
断言是任何一个xunit框架的核心,nunit中的Assert类,它提供一系列丰富的静态方法来供我们调用.如果一个断言失败,这个方法不会返回但是会报告一个错误,那么断言之后的代码就不会被执行,因此,最 ...
- 华为2022数字芯片笔试题
单选 1.ASIC开发流程中,如下环节的先后顺序是? A. RTL-> Synthesis->P&R B. Synthesis->P&R->RTL C. Syn ...
- SVA 断言 note
断言概念 一般,断言是基于时序逻辑的,单纯进行组合逻辑的断言很少见,因为太费内存(时序逻辑是每个时钟周期判断一次,而组合逻辑却是每个时钟周期内判断多次,内存吃不消). 因此,写断言的一般规则是: ti ...
- python try命令_python try语句(try/except/else/finally) Assertions
在python中,try/except语句也主要是用于处理程序正常执行过程中出现的一些异常情况,常见的异常如下: python程序在发现了except之后的某个错误时,往往会中断不再向下执行 try/ ...
- 7.3Assertions and Defensive Programming断言与防御式编程
7.3Assertions and Defensive Programming断言与防御式编程 1.回忆:设计ADT 2.Assertions 声称 --What to Assert and What ...
- UVM中SVA使用指南
UVM中SVA使用指南 文章目录 UVM中SVA使用指南 前言 一.SVA是什么,什么时候使用SVA 二.SVA块 三.SVA块嵌入UVM平台 3.1 绑定方法 3.2 例化方法 四.SVA语法浅讲 ...
最新文章
- 6、Power Query-SQL与PQ技术的强强联合
- 从 setNeedsLayout 说起
- 心电图计算心率公式_心电图到底能反应啥问题,看过之后你也能当“医生”
- 动手学深度学习(PyTorch实现)(七)--LeNet模型
- Q - Tour - hdu 3488(最小匹配值)
- LeetCode 792. 匹配子序列的单词数(Number of Matching Subsequences)
- php常用编码,简介常见的编码方式
- html——inline、block与block-inline区别
- 【bzoj3514】Codechef MARCH14 GERALD07加强版
- html5 ios keychain,ios Keychain KeychainItemWrapper
- ADS软件仿真实例大战(一)
- u盾如何在计算机上使用方法,u盾在电脑中具体使用操作过程
- Android HTTP网络详解
- VScode 本地或远程单文件和多文件调试精简配置
- 跨行入测绘,看航测小白如何实现纯免相控作业
- Qt创建线程两种方式的区别
- FinTech创业的两大势力,以及他们各有千秋的数据应用模式 | TCFA纽约年会直击
- mysql外键约束分数_MySQL 高级查询
- CAN总线多节点通信异常分析及解决
- 格式转换器:格式工厂