Property layer is built on top of sequence layer. It uses zero or more sequence to check a design assumption. zero assertions because, property layer can contain boolean layer directly. In order to use the behavior for verification, an assert, assume, or cover statement must be used. A property declaration by itself does not produce any result. Result of a property like in the case of a sequence is either true or false.

Properties can be declared in following places.

• module
• interface
• program
• clocking block
• package
• A compilation Unit

Properties can have following kinds.

• A sequence
• Negation
• Disjunction
• Conjunction
• if..else
• implication
• Another named property

A property can be simple sequence expression, as loong as it is not a empty match. Below is a simple example of this kind of property.

  1 //+++++++++++++++++++++++++++++++++++++++++++++++++
  2 //   DUT With assertions
  3 //+++++++++++++++++++++++++++++++++++++++++++++++++
  4 module propseq_assertion();
  5 
  6 logic req,gnt,clk;
  7 //=================================================
  8 //  Clock generator
  9 //=================================================
 10 initial begin
 11  clk = 0; 
 12  forever  #1  clk ++;
 13 end
 14 //=================================================
 15 // Simple DUT behaviour
 16 //=================================================
 17 always @ (posedge clk)
 18   gnt <= req;
 19 //=================================================
 20 // Test Vector generation
 21 //=================================================
 22 initial begin
 23   req <= 0;
 24    #3  req <= 1;
 25    #5  req <= 0;
 26    #1  $finish;
 27 end
 28 //=================================================
 29 // A sequence property
 30 //=================================================
 31 property propseq_prop;
 32   @ (posedge clk)
 33     req  ##1  gnt;
 34 endproperty
 35 //=================================================
 36 // Assertion Directive Layer
 37 //=================================================
 38 propseq_assert : assert property (propseq_prop);
 39 
 40 endmodule

 "propseq_assertion.sv", 38:
  propseq_assertion.propseq_assert: started at 1s failed at 1s
         Offending 'req'
 "propseq_assertion.sv", 38: 
 propseq_assertion.propseq_assert: started at 3s failed at 3s
         Offending 'req'

Copyright © 1998-2014

Deepak Kumar Tala - All rights reserved

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