Built-in functions for nondeterminism (issue 31) -- draft LRM changes

Here are the proposed LRM changes for adding the nondeterminism functions.

Page 13, Table 1:
----------------------
Add the following keywords: nondet, nondet_vector, nondet_range

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(), nondet_vector(), and nondet_range()
all have to do with nondeterministic choice of a value."

(iii)
Page 37, after section 5.2.3.8: add three new sections for the three new
operators

"5.2.3.9 nondet()
The built-in function nondet() takes two or more arguments.
It performs nondeterministic choice among the arguments, and returns the chosen value.
The arguments must all be of the same underlying HDL type, and 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 one Number argument.
If the argument to nondet_vector() is /k/, it returns a BitVector value of /k/ bits, where each bit value is chosen
nondeterministically between the values 0 and 1.

The function nondet_vector() can be used anywhere a BitVector value is required.

The argument of nondet_vector() must be a positive Number that is statically evaluatable.

5.2.3.11 nondet_range()
This function accepts two Number arguments.
If the first argument is /i/ and the second is /j/, nondet_range() chooses a Number value /x/ nondeterministically
in the range i <= x <= j, and returns the chosen value.

The function nondet_range() can be used anywhere that a Number value is required.

The arguments of nondet_vector() must be statically evaluatable. The first argument must be less than or equal to the
second argument."

Section A.4.7 Forms of expression
----------------------------------
Page 107, lines 19-29

Built_In_Function_Call ::=
prev (Any_Type [ , Number ] )
| next ( Any_Type )
...
| onehot0 ( BitVector )
| nondet (Any_Type, Any_Type {,Any_Type}) <--- NEW
| nondet_vector (Number) <--- NEW
| nondet_range (Number RANGE_SYM Number) <--- NEW

_______________________________________________________
Avigail Orni
Verification and Testing Solutions Group
IBM Haifa Research Laboratory
Phone: 972-4-829-6396 email: ornia@il.ibm.com
Received on Wed Dec 29 02:22:45 2004