System Verilog Assertions - Implication Operators

Same Cycle Implication ( |->) :

Only under certain conditions assertions may be valid.

exp1 |-> exp2 ;


If exp1 is true then exp2 must be true at the same evaluation point.

Example :

property SameCyImp

@(negedge CLK) (REQ && ~ACK) |-> BUSY ;

endproperty

assert property (SameCyImp);


Next Cycle Implication ( |=>) :

exp1 |=> exp2;

If exp1 is true , then exp2 must be true at the next evaluation point.

Example :

property NextCyImp

@(negedge CLK) (REQ && ~ACK) |=> BUSY;

endproperty

assert property (NextCyImp);





Hope, this blog is helpful to understand the use case of Same Cycle and Next Cycle Implication Operators clearly.


Please feel free to like/share/comment and follow VLSI Excellence for more such interesting blog posts.

Thanks !!!




-------------------------------------------------------------Happy Learning------------------------------