Subject: [sv-ac] written proposal: sem5
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Sun Feb 23 2003 - 03:48:08 PST
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
This archive was generated by hypermail 2b28 : Sun Feb 23 2003 - 03:48:09 PST