RE: Built-in functions for nondeterminism -- revised proposal

Avigail,

The inclusion of ranges (e.g., 1..2, or in Verilog 1:2) as parameters to these functions looks strange to me, since no languages that I know of allow this (although I gather your examples imply that GDL may do so). I would be more comfortable with the syntax if one parameter was a set of values, in which ranges could be used to define members of the set, as is common in at least Pascal and some other programming languages. In fact, you mention that one of the forms of parameter list is the "Value Set" form, but you don't appear to use the nonterminal "Value_Set" in the grammar. I would like the syntax better if we required the use of Value_Set syntax, just as in forall.

This leads me to suggest a tighter integration with the existing 'forall' syntax:

1. Extend the existing productions for Value_Set, Value_Range, and Value to include AnyType:

This gives the following syntax (with the changes from PSL v1.1 marked):

    Value_Set ::=
        '{' Value_Range { ',' Value_Range } '}'
      | 'boolean'

    Value_Range ::=
        Value
      | /finite/_Range

    Value ::=
        Boolean
      | Number
      | AnyType <== new

    Range ::=
        Low_Bound RANGE_SYM High_Bound

    Low_Bound ::=
        Number
      | MIN_VAL
      | AnyType <== new

    High_Bound ::=
        Number
      | MAX_VAL
      | AnyType <== new

    Count ::=
        Number
      | /numeric/_Range <== /numeric/ qualifer added

2. Restrict the existing uses of Range to numeric ranges, where necessary.

The /numeric/ qualifier added to the Count production above is part of this. We would also have to state that in the appropriate informal semantics sections that a /finite/_Range or /finite_positive/_Range used in FL_Property productions must be a numeric range.

The nonterminal /finite/_Range is also used in the grammar for forall. However, Issue 47 (http://www.eda.org/ieee-1850/Issues/Issues.html#47) asks for typed forall parameters, and this could be addressed by allowing the /finite/_Range used in the production for 'forall' (and also in 'for') to be non-numeric (although if the forall or for parameter is used as a Count or Range in an FL_Property, it would still need to be numeric for such references to be legal).

Finally, we should state that the bounds of a Range must be of the same type, and that the Values in a Value_Set must all be of the same type, if either is not already said.

3. Use Value_Set in the definition of the nondet functions:

    Built_In_Function_Call ::=
        prev (Any_Type [ , Number ] )
      | next ( Any_Type )
        ...
      | onehot0 ( BitVector )
      | nondet ( Value_Set ) <--- NEW (but now Value_Set)
      | nondet_vector ( Number, Value_Set ) <--- NEW (but now Value_Set)

Give the above, your examples would appear as follows:

    nondet( {0,1} )
    nondet( {1:2,4,15:18} )
    nondet( boolean )
    nondet( {BUSY,IDLE,ACCEPT} )

which echoes the current syntax for forall:

    forall i in {0:1}: P(i);
    forall n in {1:2,4,15:18}: P(n);
    forall b in boolean: P(b);
    forall v in {BUSY,IDLE,ACCEPT}: P(v); <== assuming typed 'forall' is allowed

and which I believe is being followed in the definition of 'for':

    (for i in {0:1}: && P(i))
    (for n in {1:2,4,15:18}: || P(n))
    {for b in boolean: & S(b)}
    {for v in {BUSY,IDLE,ACCEPT}: | S(v)} <== assuming typed 'for' is allowed

One possible objection to this might occur. Since both Value_Set and Sequence involve braces, the syntax for a Value_Set might be confused with that of a sequence, especially when enumeration values are involved. In fact, if more than one enum value is involved in a Value_Set, the comma (instead of a semicolon) would make it clear that it is a Value_Set, not a Sequence. Also, although a single value in braces, such as {True}, would be interpretable both as a Value_Set and as a Sequence, the context would make it clear whether a Sequence or a Value_Set is required. In any case, the problem already exists, in that it is possible to say "forall i in {True}: ...", so the issue is not a new one.

Would this refinement of your proposal be acceptable?

Regards,

Erich

| -----Original Message-----
| From: owner-ieee-1850-extensions@eda.org
| [mailto:owner-ieee-1850-extensions@eda.org] On Behalf Of Avigail Orni
| Sent: Sunday, January 23, 2005 8:01 AM
| To: ieee-1850-extensions@eda.org
| Subject: 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 20:56:46 2005