蕴含（Implication）：等效于一个if—then结构，蕴含的左边叫做“先行算子”，右边叫做“后续算子”，先行算子是约束条件，当先行算子成功时后续算子才会被计算，如果先行算子不成功，那么整个属性就默认为成功，叫做“空成功”。
注意：蕴含结构只能在属性(property)定义中，不能在序列（sequence）中使用。
- 交叠蕴含，符号“|->”，表示如果先行算子匹配，在同一个时钟周期计算后续算子表达式。
property p1;
@(posedge clk) fish_married |-> fish_baby;
endproperty
a8:assert property(p1);
属性p1检查信号"fish_married"在给定的时钟上升沿是否为高电平，如果"fish_married"为高，信号“fish_baby”在相同的时钟沿也必须为高；
- 非交叠蕴含，符号"|=>"，表示如果先行算子匹配，在下一个时钟周期计算后续算子表达式。
property p2;
@(posedge clk) fish_married |=> fish_baby;
endproperty
a9: asseert property(p2);
属性p2检查信号"fish_married"在给定的时钟上升沿是否为高电平，如果fish_married为高，信号“fish_baby”在下一个时钟沿也必须为高；
- 带固定延迟的蕴含
property p3;
@（posedge clk） fish_married |-> ##2 fish_baby;
endproperty
a10: assert property(p3);
属性p3检查信号"fish_married"在给定的时钟上升沿是否为高电平，如果"fish_married"为高，信号“fish_baby”在两个时钟周期后（##2）也为高，则断言成功。
- 使用序列作为先算子的蕴含
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将不被检查，属性检查得到一次空成功。
好了，今天的学习分享就到这里了，个人愚见，希望对你的学习有一点帮助，如有错误也欢迎批评指正。持续更新，欢迎关注。觉得有帮助的朋友，希望能够点个赞鼓励一下！！你的每个鼓励都是我持续创作的动力！
