Subject: Re: [sv-ac] written proposal: sem5
From: dudani@us04.synopsys.com
Date: Mon Feb 24 2003 - 08:24:40 PST
Hi Cindy,
What happens if the dynamic variable gets used before assignment. Do we
consider it as 'x' or an error condition?
Surrendra
At 01:48 PM 2/23/2003 +0200, you wrote:
>all,
>
>here is my written proposal for sem5, as per the meeting on thursday. note
>that the current title of sem5 is no longer appropriate. i suggest the
>following title: "separate dynamic variable declaration from assignment
>and use".
>
>proposal:
>
>separate the declaration of a dynamic variable from its assignment and use.
>declaration will be at the property level, scope is anywhere within that
>property. syntax for declaration is (type identifier_list) before a
>property. syntax for assignment is "identifier = expression". an
>assigment can appear anywhere that a boolean expression can appear, and
>evaluates to "1".
>
>examples:
>
>property p1 (int x) (valid_in) => (x = pipe_in ;[5] pipe_out1 == x+1);
>
>property p2 (int x,y) (valid_in) => (x = pipe_in ;[5] pipe_out1 == x+1;
>(pipe_out1 != pipe_cont) or (y = x+1 and ([3] pipe_out2 == y + pipe_val)));
>
>note: i based these on the examples in the dwg doc, but i haven't put a
>lot of thought into whether they are identical to what was intended there.
>so please don't read too much into the fact that they may remind you of
>those examples. the second example could also be written as:
>
>property p2a (int x) (valid_in) => (x = pipe_in ;[5] pipe_out1 == x+1;
>(pipe_out1 != pipe_cont) or ([3] pipe_out2 == x + 1 + pipe_val));
>
>so a more realistic example using two variables in the same property might
>be:
>
>property p3 (int x,y) (valid_in) => (x = pipe_tophalf_in && y =
>pipe_bottomhalf_in; [5] pipe_out1 == x; pipe_out2 == y);
>
>i am not a bnf expert, but i will take a crack at writing down what i mean
>in that format:
>
>sequence_element ::=
> boolean_expr
> | '(' sequence_expr ')'
> | identifier '=' expression
>
>clocked_expr ::=
> [event_control] [ '(' type identifier { ',' identifier } ')' ] '('
>prop_expr ')'
>
>where i have based sequence_element on the bnf of sequence_element that
>appears in revision 0.79, and clocked_expr on the bnf of clocked_expr that
>appears in the ballot for "sem1".
>
>note that "identifier = expression" is a sequence_element, but always
>evaluates to '1' (as described above). therefore, it doesn't change the
>meaning of the sequence other than causing a "sampling" of the expression
>into the dynamic variable.
>
>regards,
>
>cindy.
>
>Cindy Eisner
>Formal Methods Group Tel: +972-4-8296-266
>IBM Haifa Research Laboratory Fax: +972-4-8296-114
>Haifa 31905, Israel e-mail:
>eisner@il.ibm.com
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive
Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Mon Feb 24 2003 - 08:25:30 PST