Implication kind property is kind of similar to if..else kind property. What implication does is, it checks for the preceding sequence to occur to check behaviour.

Below is the syntax of implication property.

sequence_expr |-> property_expr
sequence_expr |=> property_expr

The result of the implication is either true or false. The left-hand operand sequence_expr is called the antecedent, while the right-hand operand property_expr is called the consequent.

Rules of implication operator

• From a given start point, the antecedent sequence_expr can have zero, one, or more than one successful match.
• If there is no match of the antecedent sequence_expr from a given start point, then evaluation of the implication from that start point succeeds vacuously and returns true.
• For each successful match of antecedent sequence_expr, the consequent property_expr is separately evaluated. The end point of the match of the antecedent sequence_expr is the start point of the evaluation of the consequent property_expr.
• From a given start point, evaluation of the implication succeeds and returns true if, and only if, for every match of the antecedent sequence_expr beginning at the start point, the evaluation of the consequent property_expr beginning at the end point of the match succeeds and returns true.

There are two types of implication operator as shown in above syntax.

• |-> : Overlapped implication operator. If there is a match for the antecedent sequence_expr, then the end point of the match is the start point of the evaluation of the consequent property_expr.
• |=> : Non Overlapped implication operator. The start point of the evaluation of the consequent property_expr is the clock tick after the end point of the match.

Below example shows the difference between |-> and |=> and application of implication operator.

  1 //+++++++++++++++++++++++++++++++++++++++++++++++++
  2 //   DUT With assertions
  3 //+++++++++++++++++++++++++++++++++++++++++++++++++
  4 module implication_assertion();
  5 
  6 logic clk = 0;
  7 always  #1  clk ++;
  8 
  9 logic req,busy,gnt;
 10 //=================================================
 11 // Sequence Layer
 12 //=================================================
 13 sequence implication_seq;
 14   req  ##1  (busy [->3])  ##1  gnt;
 15 endsequence
 16 
 17 //=================================================
 18 // Property Specification Layer
 19 //=================================================
 20 property overlap_prop;
 21   @ (posedge clk) 
 22       req |-> implication_seq;
 23 endproperty
 24 
 25 property nonoverlap_prop;
 26   @ (posedge clk) 
 27       req |=> implication_seq;
 28 endproperty
 29 //=================================================
 30 // Assertion Directive Layer
 31 //=================================================
 32 overlap_assert    : assert property (overlap_prop);
 33 nonoverlap_assert : assert property (nonoverlap_prop);
 34 
 35 //=================================================
 36 // Generate input vectors
 37 //=================================================
 38 initial begin
 39   // Pass sequence
 40   gen_seq(3,0); 
 41   repeat (20) @ (posedge clk);
 42   // Fail sequence (gnt is not asserted properly)
 43   gen_seq(3,1); 
 44   // Terminate the sim
 45    #30  $finish;
 46 end
 47 //=================================================
 48 /// Task to generate input sequence
 49 //=================================================
 50 task  gen_seq (int busy_delay,int gnt_delay);
 51   req <= 0; busy <= 0;gnt <= 0;
 52   @ (posedge clk);
 53   req <= 1;
 54   @ (posedge clk);
 55   req  <= 0;
 56   repeat (busy_delay) begin
 57    @ (posedge clk);
 58     busy <= 1;
 59    @ (posedge clk);
 60     busy <= 0;
 61   end
 62   repeat (gnt_delay) @ (posedge clk);
 63   gnt <= 1;
 64   @ (posedge clk);
 65   gnt <= 0;
 66 endtask
 67 
 68 endmodule

 "implication_assertion.sv", 33: 
 implication_assertion.nonoverlap_assert: started at 3s failed at 5s
         Offending 'req'
 "implication_assertion.sv", 33: 
 implication_assertion.nonoverlap_assert: started at 61s failed at 63s
         Offending 'req'
 "implication_assertion.sv", 32: 
 implication_assertion.overlap_assert: started at 61s failed at 75s
         Offending 'gnt'
 $finish called from file "implication_assertion.sv", line 45.

Copyright © 1998-2014

Deepak Kumar Tala - All rights reserved

Do you have any Comment? mail me at:deepak@asic-world.com