SV |
您所在的位置：网站首页 › 下降沿verilog符号 › SV |
SV
|
SV – Assertions 断言
文章目录
SV -- Assertions 断言1.简介1.1 立即断言
2.SVA (system verilog assertion)2.1 Sequence2.2 Property2.2.1 implication2.2.2 repetition 重复操作2.2.3 go to repetition 跟随重复2.2.4 Nonconsecutive repetition 非连续重复2.2.5 throughout2.2.6 within
2.3 SVA 方法2.3.1 $rose2.3.2 $fell2.3.3 $stable2.3.4 $past2.3.5 内置系统方法2.3.6 disable iff2.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 generation
always #5 clk = ~clk;
//generating 'a'
initial begin
a=1;
b=1;
#15 b=0;
#10 b=1;
a=0;
#20 a=1;
#10;
$finish;
end
//Immediate assertion
always @(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; endsequence property p; @(posedge clk) seq; endproperty a_1 : assert property(p); 2.2 Propertyproperty也可以像sequence一样定义参数，同时也可以在property内部定义变量，如： int a; 另外，如果这么写 a_3: assert property(@(posedge clk) p) ，如果p中也有clk语句，则不允许。 not的写法： sequence seq; @(posedge clk) a ##2 b; endsequence property p; not seq; endproperty a_1: assert property(p);not表示断言的内容不发生，也就是要么a不为1，要么a为1但延时2以后b还不为1. 2.2.1 implicationimplication只能在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 ) ); endproperty a31: 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 begin cfg_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 property a_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 |
【本文地址】
今日新闻 |
推荐新闻 |