Built-in functions for nondeterminism -- using Value_Set

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:34:44 2005