Subject: Correction : [sv-ac] proposal for #7 of v3.1 (support parameters for assertions)
From: Joseph Lu (Juin-Yeu.Lu@sun.com)
Date: Thu Sep 11 2003 - 08:45:09 PDT
Hi,
Some corrections on the proposal for the support of parameters for assertions.
BNF:
property_declaration::=
property property_id [property_formal_list] ;
{ parameter_declaration }
{ assertion_variable_declaration }
property_spec;
endproperty [:property_id]
parameter_declaration ::=
parameter_list;
parameter_list ::= parameter_statement {; parameter_statement }
parameter_statement ::= int_para | bool_para | clock_event_para | sequence_para;
int_para ::= parameter int para_id = int_value;
bool_para ::= parameter bool para_id = bool_value;
clock_event_para ::= parameter clock_event para_id = clock_event_kind;
clock_event_kind ::= posedge | negedge | edge;
sequence_para ::= parameter sequence para_id = sequence_exp;
Example:
property follow(en, clk, leader, follower);
parameter int min_lat = 0;
parameter int max_lat = 0;
parameter clock_event = posedge;
@(clock_event 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");
Comments and questions are very welcome.
Thanks,
Joseph Lu
>Date: Wed, 10 Sep 2003 17:53:48 -0700 (PDT)
>From: Joseph Lu <joseph@ha1sun-mail1>
>Subject: [sv-ac] proposal for #7 of v3.1 (support parameters for assertions)
>To: sv-ac@eda.org
>Cc: Joseph Lu <Juin-Yeu.Lu@Sun.COM>
>MIME-version: 1.0
>Content-MD5: 7GJ3+CKuMROSRFKsZ8n0PQ==
>Original-recipient: rfc822;Juin-Yeu.Lu@Sun.COM
>
>
>Hi,
>
>This is the draft proposal for the support of parameters for assertions.
>
>
>Proposal : parameter value assignment
>
> - allow parameter value passing by position as well as by name
> - if parameter value passing is by name, actual parameters can be
> in any order in the parameter list and parameters can be omitted.
> - if parameter value passing is by position, the order of actual parameters
> need to be the same as that of the formal parameters and actual parameters
> can not be skipped. To skip a subset of parameters with this method,
> in the parameter declaration, this subset shall be preceded by
> the remaining parameters.
>
> - allow to pass int constant, boolean, clk_event, sequence and etc.
>
>BNF:
>
>property_declaration::=
>
> property property_id [property_formal_list] ;
> { parameter_declaration }
> { assertion_variable_declaration }
> property_spec;
>
> endproperty [:property_id]
>
> parameter_declaration ::=
> parameter_list;
>
> parameter_list ::= parameter_statement {; parameter_statement }
> parameter_statement ::= parameter_kind parameter_id = parameter_value;
> parameter_kind ::= int | bool | clock_event | sequence
> clock_event ::= posedge | negedge | edge
>
>Example:
>
>property follow(en, clk, leader, follower);
> parameter int min_lat = 0;
> parameter int max_lat = 0;
> parameter clock_event = posedge;
>
> @(clock_event ck) en |-> (`true [*0:$] ##1 leader ##[min_lat:max_lat] follower) [*1:$] ;
>
>endproperty
>
>// SVA follow instance
>follow_posedge : assert property ( #(min_lat=3,max_lat=5,clock_event=netsedge ) follow(en, clk,
>leader,follower))
> ;
> else $display("%m follower reponses late");
>
>
>
>Comments and questions are very welcome.
>
>Thanks,
>
>
>--------------------------------------------------
>Joseph Lu, Ph.D.
>Processor Product and Network Group
>Sun Microsystems
>M/S USUN 03-202, 430 N. Mary Ave.,
>Sunnyvale, CA 94086
>408-616-5887
>Juin-Yeu.Lu@Sun.COM
>--------------------------------------------------
>
This archive was generated by hypermail 2b28 : Thu Sep 11 2003 - 08:45:49 PDT