• If we want the sequence to be checked only after “a” is high, this can be achieved by using the implication operator. The implication is equivalent to an if-then structure.

• The left-hand side of the implication is called the “antecedent” and the right-hand side is called the “consequent.”

• It can be used only with property definitions not used with sequences.

• There are two types of implication operators:

1. Overlapped implication (|->)
2. Non-overlapped implication (|=>)

                             Fig.1 Implication Operators in Assertions

• It is denoted by |->.
• If there is a match on the antecedent, then the consequent expression is evaluated in the same clock cycle.

Syntax:-
<Antecedent> |-> <Consequent>

Example:-
property p;
@(posedge clk) a |-> b;
endproperty
a: assert property(p);

In the above example when "a" is high on the positive edge of clock cycle then "b" will be evaluated and based on that assertion will be passed or fail.

                   Fig.2 Overlapped Implication

Code snippet:

  module overlapped_assertion;
  bit clk,a,b,valid;

  always #5 clk = ~clk; //clock generation

  //generating 'a'
  initial begin
    valid=1; a=1; b=1;
   #15 a=1; b=0;
   #10 b=1;
   #10 b=0;
   #10 a=0; b=1;
    valid=0;
   #15 a=1; b=0;
   #100 $finish;
  end
 
  // property definition
  property p;
    @(posedge clk) valid |-> (a ##3 b);
  endproperty

 //calling assert property
   a_1: assert property(p)
     $info("pass");
     else
      $info("fail");

 endmodule

Output:

The below figure will shows the overlapped implication output. here, at 5ns first posedge comes and at that point valid and a both are high so it will check for b after 3 clock cycles at 35ns b is high so assertion passed if b is not high at that point then assertion is fail and this same process will be followed for other posedges till $finish is called.

                                Fig.3 Output of overlapped implication

• Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” should be high after 2 clock cycles.
• Fixed delay can be denoted as ##n here n will specify the time.

Syntax:-
<Antecedent> |-> ##<value> <Consequent>

Example:-
property p;
@(posedge clk) a |-> ##2 b;
endproperty
a: assert property(p);

             Fig.4 Fixed Delay  

• Below property checks that, if the sequence seq_1 is true on a given positive edge of the clock, then start checking the seq_2 (“d” should be low, 2 clock cycles after seq_1 is true).

Syntax:-
<Sequence1> |-> <Sequence2>

Example:-
sequence seq_1;
(a && b) ##1 c;
endsequence

sequence seq_2;
##2 !d;
endsequence

property p;
@(posedge clk) seq_1 |-> seq_2;
endpeoperty
a: assert property(p);

• Below property checks that, if signal “a” is high on a given positive clock edge, then within 1 to 3 clock cycles, the signal “b” should be high.

Syntax
<Antecedent> |-> ##[1:<value>] <Consequent>

Example:-
property p;
@(posedge clk)
a |-> ##[1:3] b;
endproperty
a: assert property(p);

            Fig.4 Timing Window  

• Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” should be high in the same clock cycle or within 4 clock cycles.

Syntax:-
<Antecedent> |-> ##[0:<value>] <Consequent>

Example:-
property p;
@(posedge clk)
a |-> ##[0:4] b;
endproperty
a: assert property(p);

            Fig.5 Overlapping Timing Window

• The upper limit of the timing window specified in the right-hand side can be defined with a “$” sign which implies that there is no upper bound for timing. This is called the “eventuality” operator. The checker will keep checking for a match until the end of the simulation.
• Below property checks that, if signal “a” is high on a given positive clock edge, then signal “b” will be high eventually starting from the next clock cycle.

Syntax:-
<Antecedent> |-> ##[1:$] <Consequent>

Example:-
property p;
@(posedge clk)
a |-> ##[1:$] b;
endproperty
a: assert property(p);

             Fig.6 Indefinite Timing Window  

• The non-overlapped implication is denoted by the symbol |=>.
• If there is a match on the antecedent, then the consequent expression is evaluated in the next clock cycle.

Syntax:-
<Antecedent> |=> <Consequent>

Example :-
property p;
@(posedge clk) a |=>b;
endproperty
a: assert property( p );

In the above example if signal “a” is high on a given positive clock edge, then signal “b” should be high on the next clock edge.

            Fig.7 Non-Overlapped Implication

Output:

The below figure will shows the nonoverlapped implication output. here, at 5ns first posedge comes and at that point valid is high after one clock cycle at 15ns a is high so it will check for b after 3 clock cycles at 45ns b is high so assertion passed if b is not high at that point then assertion is fail and this same process will be followed for other posedges till $finish is called.

                                Fig.3 Output of nonoverlapped implication