Subject: Re: [sv-ac] Re: proposal for parameters on properties.
From: Joseph Lu (Juin-Yeu.Lu@sun.com)
Date: Thu Sep 18 2003 - 11:08:26 PDT
Hi Adam,
This is good!!,
But, one more thing, i am not clear about if the range of local variables for properties needs
to be compile-time constants. I believe that is why parameters are for in SV.
In addition, the repetition expression requires either a constant or a range.
If we are using existing SVA 3.1 approach, I can easily make a mistake by hooking up
a signal to an actual parameter for a range identifier.
Maybe this can be dealt by the tool implementation. Any thought on this ?
Thanks Adam.
--Joseph
>Date: Thu, 18 Sep 2003 09:21:19 -0500
>From: Adam Krolnik <krolnik@lsil.com>
>Subject: [sv-ac] Re: proposal for parameters on properties.
>To: Joseph Lu <Juin-Yeu.Lu@Sun.COM>
>Cc: sv-ac@eda.org
>MIME-version: 1.0
>Content-transfer-encoding: 7bit
>X-Accept-Language: en-us, en
>User-Agent: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.2.1) Gecko/20030711
>
>
>
>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 - 11:09:23 PDT