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

Dear Avigail,

we should avoid complicating the language by additional functions, if we can.

It seems to me that one construct would be sufficient, namely a way to
*declare* new, free variables.
I am not sure but this seems to lack currently from PSL.

Am I mistaken, or would
        declare x: integer;
        assume a <= x and x <= b;
have the same effect as
        x= nondet_range(a,b);
?

Similar alternatives seem to exist for the other suggested functions.
What is your opinion?

Regards
Klaus

>---------------------------------------------------------------------
>Dr. Klaus Winkelmann
>Infineon Technologies AG, Corporate Logic
>Formal Verification, CL D DAT DF V
>81730 München
>Tel. +49-89-234-41125
>Fax +49-89-234-955 7111
>Mobil +49-170-5625455
>Klaus.Winkelmann@infineon.com
>---------------------------------------------------------------------
>
>

-----Ursprüngliche Nachricht-----
Von: owner-ieee-1850@eda.org [mailto:owner-ieee-1850@eda.org] Im Auftrag von Avigail Orni
Gesendet: Montag, 20. Dezember 2004 14:10
An: ieee-1850@eda.org
Betreff: [$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 Tue Dec 21 04:04:12 2004