SVA学习|05. 蕴含操作符

蕴含（Implication）：等效于一个if—then结构，蕴含的左边叫做“先行算子”，右边叫做“后续算子”，先行算子是约束条件，当先行算子成功时后续算子才会被计算，如果先行算子不成功，那么整个属性就默认为成功，叫做“空成功”。

注意：蕴含结构只能在属性(property)定义中，不能在序列（sequence）中使用。

1. 交叠蕴含，符号“|->”，表示如果先行算子匹配，在同一个时钟周期计算后续算子表达式。

property p1;
    @(posedge clk)    fish_married |-> fish_baby;
endproperty
 
a8:assert property(p1);

属性p1检查信号"fish_married"在给定的时钟上升沿是否为高电平，如果"fish_married"为高，信号“fish_baby”在相同的时钟沿也必须为高；

1. 非交叠蕴含，符号"|=>"，表示如果先行算子匹配，在下一个时钟周期计算后续算子表达式。

property p2;
    @(posedge clk)  fish_married |=> fish_baby;
endproperty
 
a9: asseert property(p2);

属性p2检查信号"fish_married"在给定的时钟上升沿是否为高电平，如果fish_married为高，信号“fish_baby”在下一个时钟沿也必须为高；

1. 带固定延迟的蕴含

property p3;
    @（posedge clk）    fish_married |-> ##2 fish_baby;
endproperty
 
a10: assert property(p3);

属性p3检查信号"fish_married"在给定的时钟上升沿是否为高电平，如果"fish_married"为高，信号“fish_baby”在两个时钟周期后（##2）也为高，则断言成功。

1. 使用序列作为先算子的蕴含

sequence s1a;
    @(posedge clk) (fish && married) ##1 fish_baby;
endsequence
 
sequence s1b;
    @(posedge clk)  ##2 fish_sec_baby;
endsequence
 
property p4;
    s1a |-> slb;
endproperty

序列s1a检查如果信号“fish”和信号“married”都为高，一个时钟周期后信号“fish_baby”应该为高；序列是s1b检查当前时钟上升沿的两个时钟周期后，信号“fish_sec_baby”应为高。属性p4检查如果序列s1a成功，那么序列s1b被检查，如果没有监测到有效的s1a，那么序列s1b将不被检查，属性检查得到一次空成功。

好了，今天的学习分享就到这里了，个人愚见，希望对你的学习有一点帮助，如有错误也欢迎批评指正。持续更新，欢迎关注。觉得有帮助的朋友，希望能够点个赞鼓励一下！！你的每个鼓励都是我持续创作的动力！