Corrections: Built-in functions for nondeterminism -- using Value_Set

I've just noticed two places in my previous email that require correction:

(1) In the proposed section 5.2.3.9 (nondet)
> The function nondet() performs nondeterministic choice among the values
in
> the Value Set, and returns the chosen value. The value returned is of the
> same type as the arguments.

Should be:
"The value returned is of the same type as the Value Set elements".

(2) In the proposed section 5.2.3.10 (nondet_vector)
> If the type of the arguments is /T/, then the function nondet_vector()
can
> be used anywhere that an array of length /k/ with elements of type /T/ is
> allowed.

Should be:
"If the type of the Value Set elements is /T/, then ... "

_______________________________________________________
Avigail Orni
Verification and Testing Solutions Group
IBM Haifa Research Laboratory
Phone: 972-4-829-6396 email: ornia@il.ibm.com
----- Forwarded by Avigail Orni/Haifa/IBM on 30/01/2005 15:45 -----

owner-ieee-1850-extensions@eda.org wrote on 30/01/2005 15:38:36:

>
>
>
>
> Hi all,
>
> Here is another proposal for the nondetermininsm functions, based on
> Erich's suggestion to use a Value_Set parameter. This proposal includes:
>
> (1) addition of the nondet() and nondet_vector() built-in functions
> (2) extension of Value_Set to include Any_Type (this affects nondet*(),
> 'forall', and 'for')
> (3) changes to 'forall' and 'for' sections due to the addition of
Any_Type
> to Value_Set
>
> It seems to me that the changes to the grammar are independent of the
> changes in Dana's proposal.
>
> ---------------------------------------------------------
>
> Detailed LRM changes:
>
>
> Page 13, Table 1:
> ----------------------
> Add the following keywords: nondet, nondet_vector
>
>
> Section 5.2.3 Built-in Functions
> ---------------------------------
> (i)
> Page 33, line 55: replace the following sentence
> "PSL defines a collection of built-in functions that detect typically
> interesting conditions."
> with
> "PSL defines a collection of built-in functions that detect typically
> interesting conditions, or compute useful values."
>
> (ii)
> Page 34, lines 17-19: the existing text refers to two classes of built-in
> functions. In order to include the new functions, replace with the
> following text:
> "There are three classes of built-in functions. Functions prev(), next(),
> stable(), rose(), and fell()
> all have to do with the values of expressions over time. Functions
> isunknown(), countones(),
> onehot(), and onehot0() all have to do with the values of bits in a
vector
> at a given instant. Functions nondet() and nondet_vector() have to do
with
> nondeterministic choice of a value."
>
>
> (iii)
> Page 37, after section 5.2.3.8: add two new sections for the two new
> operators
>
>
> "5.2.3.9 nondet()
> The built-in function nondet() takes one Value Set argument. The set of
> values can be specified in three different ways
> — The keyword boolean specifies the set of values {True, False}.
> — A Value Range specifies the set of all Number values within the given
> range.
> — The comma (,) between Value Ranges indicates the union of the obtained
> sets.
> - A list of comma-separated values specifies a value set of arbitrary
type;
> all values must be of the same underlying HDL type"
>
> The function nondet() performs nondeterministic choice among the values
in
> the Value Set, and returns the chosen value. The value returned is of the
> same type as the arguments.
>
> If the type of the return value is /T/, then the function nondet() can be
> used anywhere that a value of type /T/ is required.
>
>
> Examples: (Optional)
>
> nondet(boolean) -- returns a value chosen nondeterministically in the
set
> {True, False}
>
> nondet( {1:2,4,15:18} ) -- returns a value chosen nondeterministically in
> the set {1,2,4,15,16,17,18}
>
>
>
> 5.2.3.10 nondet_vector()
> This function accepts two arguments. The first argument is a Number. The
> second argument is a Value Set, as specified for the nondet() function.
> If the first argument to nondet_vector() is /k/, it returns an array of
> length /k/, whose elements are chosen nondeterministically in the set of
> values described by the second argument.
>
> If the type of the arguments is /T/, then the function nondet_vector()
can
> be used anywhere that an array of length /k/ with elements of type /T/ is
> allowed.
>
> The first argument of nondet_vector() must be a positive Number that is
> statically evaluatable.
>
>
> Examples: (Optional)
>
> nondet_vector(16, boolean) -- returns an array of length 16, with each
> element chosen nondeterministically in the set {True, False}
>
> nondet(8, {1:2,4,15:18} ) -- returns an array of length 8, with each
> element chosen nondeterministically in the set {1,2,4,15,16,17,18}
>
>
>
> Section A.4.7 Forms of expression
> ----------------------------------
>
> Page 104, add at line 12
> ------------------------
> Value_Set ::=
> '{' Value_Range { ',' Value_Range } '}'
> | 'boolean'
> | '{' Any_Type { ',' Any_Type } '}' <--- NEW
>
>
>
> Page 107, lines 19-29
> ---------------------
> Built_In_Function_Call ::=
> prev (Any_Type [ , Number ] )
> | next ( Any_Type )
> ...
> | onehot0 ( BitVector )
> | nondet ( Value_Set ) <--- NEW
> | nondet_vector ( Number, Value_Set ) <--- NEW
>
>
>
> Section 6.2.3. Replicated Properties
> -------------------------------------
> (i)
> Page 80, lines 6-11: add a sentence to the existing text to include the
> Any_Type set of values
>
> "The set of values can be specified in three different ways
> — The keyword boolean specifies the set of values {True, False}.
> — A Value Range specifies the set of all Number values within the given
> range. <-- ("Number" added)
> — The comma (,) between Value Ranges indicates the union of the obtained
> sets.
> - A list of comma-separated values specifies a value set of arbitrary
type;
> all values must be of the same underlying HDL type <-- (This sentence
> added)"
> (This change should be made in Dana's proposal as well, for parameterized
> SEREs and parameterized properties)
>
> (ii)
> Page 80, after line 23: add the following paragraph
>
> "If the value set is specified by a list of values of arbitrary type,
each
> of the values must be statically computable"
> (This change should be made in Dana's proposal as well, for parameterized
> SEREs and parameterized properties)
>
> _______________________________________________________
> Avigail Orni
> Verification and Testing Solutions Group
> IBM Haifa Research Laboratory
> Phone: 972-4-829-6396 email: ornia@il.ibm.com
>
Received on Sun Jan 30 05:45:48 2005