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

Going beyond formal, non-deterministic/random variables with probability
would make sense for simulation.
Surrendra
At 01:04 PM 12/21/2004 +0100, you wrote:

>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

**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive, Suite 300
Marlboro, MA 01752

Tel: 508-263-8072
Fax: 508-263-8123
email: Surrendra.Dudani@synopsys.com
**********************************************
Received on Tue Dec 21 07:23:53 2004