[$ieee-1850] Built-in functions for expressing nondeterminism (issue 31)

Hi all,

Here is a proposal for adding nondeterminism operators to the boolean
layer, in order to address issue 31 (it is based on a similar proposal that
was made by Sitvanit for LRM 1.1).

Nondeterminism operators are necessery for model checking. The boolean
layer currently has one nondeterminism operator: union. On page 38 of the
LRM we have the following example:

"a = b union c;
This is a non-deterministic assignment of either b or c to variable or
signal a."

The problem with this operator is that it only provides a choice between
two values. If we require a choice among many values, we must write a very
long expression. For example, for a choice in the range 1..5, we must write
((((1 union 2) union 3) union 4) union 5). This becomes unreasonable if
the range is 1..100.

Therefore, we propose adding the following 3 built-in functions:

-------------------------------------------------------
nondet(a1, a2, ..., an)

This function accepts two or more arguments and performs non-deterministic choice among them.
All arguments must be of the same underlying HDL type.

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

nondet_vector(k)

This function accepts one argument of type integer.
The function returns a bitvector of k bits, where each bit value is chosen non-deterministically.
the value of the argument should be known at compile time. This value should be (strictly) positive.

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

nondet_range(a, b)

This function accepts two arguments of type integer; their values should be known at compile time.
The value of b should be greater than or equal to the value of a.
This function returns an integer value x chosen non-deterministically in the range a..b.

_______________________________________________________
Avigail Orni
Verification and Testing Solutions Group
IBM Haifa Research Laboratory
Phone: 972-4-829-6396 email: ornia@il.ibm.com
Received on Mon Dec 20 05:06:11 2004