[sv-ac] Re: proposal for parameters on properties.


Subject: [sv-ac] Re: proposal for parameters on properties.
From: Adam Krolnik (krolnik@lsil.com)
Date: Thu Sep 18 2003 - 07:21:19 PDT


Hello Joseph;

You are proposing the addition of parameters to properties for
the use of further configuration of the property itself.

You are proposing the addition of:

   o pass int constant, boolean, clk_event, sequence as parameter.

I believe all of this currently can be accomplished with the existing
interface of the property.

1. The formal parameters of the property have no type associated with them.
    Thus one can pass any verilog element through.

2. The parameters can be defined to have an initial value. This value can
    be an expression (which can be an identifier) or an event control specification.

You have an example, I would like to show how you can use the existing capability
to perform the same operation:

Your property is:

property follow(en, clk, leader, follower);
   parameter int min_lat = 0;
   parameter int max_lat = 0;
   parameter clock_event sample_clock_edge = posedge;
   @(sample_clock_edge ck)

   en |-> ( true [*0:$] ##1 leader ##[min_lat:max_lat] follower) [*1:$];
endproperty

// SVA follow instance
follow_negedge : assert property
   ( #(max_lat=5,min_lat=3,clock_event=negedge )
      follow(en, clk,leader,follower) )
  ; else $display("%m follower reponses late");

It can in 3.1 be written as:

property follow(en, leader, follower,
                 clk_event = posedge clk,
                 min_lat = 0,
                 max_lat = 0);
   @(clk_event)

   (en |-> ( true [*0:$] ##1 leader ##[min_lat:max_lat] follower) [*1:$]);
endproperty

// SVA 3.1 follow instance
follow_negedge : assert property
   (follower(.en(en),
             .clk_event(negedge clk),
             .leader(leader),
             .follower(follower),
             .min_lat(3),
             .max_lat(5))
    else $display("follower reponses late");

Changes made:
   1. Combine sample_clock_edge and clk into one parameter - clk_event.
   2. Switch to named parameter connection, instead of ordered.
   3. Removal of %m from error message - you should already get that.

I did not change the property!

One could even do this with 3.1:

   property savethis (valid, addr, AWIDTH=16, done, done_addr, max=100);
     reg [AWIDTH-1:0] save_addr;
    (valid, save_addr = addr |-> ##[1:max] done ##0 save_addr == done_addr)
   endproperty

I'm using a property parameter to specify the width of a local variable, just
   like a parameter is used for this.

Thus a property parameter can be used to do the following:

   1. Pass in a property to use.
   2. Pass in a sequence to use.
   3. Pass in a signal to use in a property/sequence.
   4. Pass in a constant for a range, repetition, count.
   5. Pass in a parameter for a range, or repetition count.
   6. Pass in a constant for a local variable size.
   7. Pass in a function call? to be used as an expression, etc?
   8. Pass in a string to be used for ?? (error message?)

What we really can't do yet is create a module containing a property and
some satellite logic and use the module instance as instantiation of the
property, etc. This won't work because of:
   o You can't pass a property or sequence through the ports of a module.

The only thing you could do would possible be this...

   module XYZmonitor(
     <ports for the property, logic, etc.>
     );

   <logic for helping the property.>

   property foo (<parameters. of the property>
   endproperty
   endmodule

   XYZmonitor m1 (<port connections>);
   assert property (m1.foo(my_property_to_use))
     else $error("Failed to match XYZ protocol.");

   assert property <for all the other properties in the monitor. Don't forget
     any, otherwise you won't be checking the property...>

Thanks Joseph;

    Adam Krolnik
    Verification Mgr.
    LSI Logic Corp.
    Plano TX. 75074
    Co-author "Assertion Based Design"



This archive was generated by hypermail 2b28 : Thu Sep 18 2003 - 08:57:50 PDT