Built-in functions for nondeterminism -- revised proposal

Hi All,

This is a revised proposal for adding the nondeterminism functions. I've
attempted to make the format more similar to the "forall" construct.

The main changes with regard to the previous proposal are:
(1) only two functions: nondet() and nondet_vector()
(2) each of these functions has three forms (two forms equivalent to
"forall", and one Any_Type form)

Here are some examples of legal usage (GDL flavor):

nondet(0,1)
nondet(1..2, 4, 15..18)
nondet(boolean)
nondet(BUSY, IDLE, ACCEPT) -- this is the Any_Type form; in this example
the values are of enum type in GDL

nondet_vector(16, boolean) -- a bitvector of length 16, with each bit
chosen nondeterministically
nondet_vector(8, 1..2, 4, 15..18) -- a vector of length 8, whose elements
are numbers in the set {1..2, 4, 15..18}
nondet_vector(4, BUSY, IDLE, ACCEPT) -- a vector of length 4, whose
elements are of enum type in GDL

------------------------------------------------------------

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 or more arguments. The argument
list may be in one of three possible forms:
(i) Value Set: used for describing a set of Number values.
Each argument is a Value Range, specifying the set of all values within the
given range; the comma (,) between Value Ranges indicates the union of the
obtained sets.
(ii) Boolean: used for specifying the set of values {True, False}.
The argument list consists of a single item, the keyword boolean.
(iii) Any Type: used for specifying a set of values of arbitrary type.
Each argument in the list specifies a single value. The arguments must all
be of the same underlying HDL type.

The function nondet() performs nondeterministic choice among its arguments,
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.

5.2.3.10 nondet_vector()
This function accepts two or more arguments. The first argument must be a
Number. The remaining arguments may be in one of the three forms allowed
for nondet() arguments.
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 remaining arguments.

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.

Section A.4.7 Forms of expression
----------------------------------

Page 104, add at line 20
------------------------
(Value_List is similar to the existing Value_Set, but does not include the
curly braces, and has the additional "Any_Type" option)

Value_List ::=
Value_Range {, Value_Range }
| boolean
| Any_Type {,Any_Type}

Page 107, lines 19-29
---------------------
Built_In_Function_Call ::=
prev (Any_Type [ , Number ] )
| next ( Any_Type )
...
| onehot0 ( BitVector )
| nondet ( Value_List ) <--- NEW
| nondet_vector ( Number, Value_List ) <--- NEW

_______________________________________________________
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 23 04:57:03 2005