As seen all the example earlier, a property in itself can not be used for checking a condition, it needs to used with verification statements like assert.

Followin are verification statements that can use a property.

• assert : This statement specifies if the propery holds correct.
• assume : This statement specifies property as assumption for the verification enviroment. This is more usefull with formal verification tools.
• cover : This statement monitors property for the sake of coverage. Coverage can be made to be reported at the end of simulation.

The assert, assume, or cover statements can be referenced by their optional name. If name is not given then compiler will give name for the sake of reporting as shown in example below.

Above verification statements can be specified in following places.

• initial or always blocks
• module
• interface
• program

  1 //+++++++++++++++++++++++++++++++++++++++++++++++++
  2 //   DUT With assertions
  3 //+++++++++++++++++++++++++++++++++++++++++++++++++
  4 module assert_assume_cover_assertion();
  5 logic clk = 0;
  6 logic req,gnt;
  7 logic ce,wr;
  8 logic [7:0] addr, data;
  9 //=================================================
 10 // Property Specification Layer
 11 //=================================================
 12 property req_gnt_prop;
 13   @ (posedge clk)
 14       req |=> gnt;
 15 endproperty
 16 //=================================================
 17 // Check if address falls in range for a write 
 18 // operation
 19 //=================================================
 20 property addr_hit_prop(int min, int max);
 21   @ (posedge clk)
 22    (ce & wr) |-> (addr >= min && addr <= max);
 23 endproperty
 24 //=================================================
 25 // Simple DUT with assert
 26 //=================================================
 27 always @ (posedge clk)
 28 begin
 29    gnt <= req;
 30    //==============================================
 31    // Assert inside a always block
 32    //==============================================
 33    req_gnt_assert : assert property (req_gnt_prop);
 34 end
 35 //=================================================
 36 // This is how you use "assume"
 37 //=================================================
 38 req_gnt_assume  : assume property (req_gnt_prop);
 39 //=================================================
 40 // This is how you use "assert"
 41 //=================================================
 42 req_gnt_assert2 : assert property (req_gnt_prop);
 43 //=================================================
 44 // This is how you use "cover"
 45 //=================================================
 46 req_gnt_cover   : cover property (req_gnt_prop);
 47 addr_hit_cover  : cover property (addr_hit_prop(1,5));
 48 //+++++++++++++++++++++++++++++++++++++++++++++++++
 49 //  Assertion testing code
 50 //+++++++++++++++++++++++++++++++++++++++++++++++++
 51 always  #1  clk ++;
 52 
 53 initial begin
 54   ce <= 0; wr <= 0; addr <= 0; req <= 0; gnt <= 0;
 55   data <= 0;
 56   // Make the assertion pass
 57   @ (posedge clk) req  <= 1;
 58   @ (posedge gnt);
 59   for (int i = 0; i < 10; i ++) begin
 60     @ (posedge clk);
 61     ce <= 1;
 62     wr <= 1;
 63     addr <= i;
 64     data <= $random;
 65     @ (posedge clk);
 66     ce <= 0;
 67     wr <= 0;
 68     addr <= 0;
 69   end
 70   @ (posedge clk);
 71   req <= 0;
 72   // Check 
 73    #10  $finish;
 74 end
 75 
 76 endmodule

 $finish called from file "assert_assume_cover_assertion.sv", line 73.
 $finish at simulation time                   55
 "assert_assume_cover_assertion.sv", 46: 
 assert_assume_cover_assertion.req_gnt_cover, 27 attempts, 22 match
 "assert_assume_cover_assertion.sv", 47: 
 assert_assume_cover_assertion.addr_hit_cover, 27 attempts, 5 match

Copyright © 1998-2014

Deepak Kumar Tala - All rights reserved

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