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

Hi Avigail,

It occurred to me that the use of AnyType in ranges might worry some people. However, I believe that can be addressed gracefully by simply stating that, if the AnyType class is used in a range, then the corresponding HDL type must be an ordered type, i.e., one for which relational operators <, > are defined. Enumeration types are generally defined such that they are ordered, so this would allow enum types.

It would also allow floating-point types. If that is troublesome, then we could further restrict AnyType in a range to include only discrete types, i.e., types whose values map onto integers.

That said, if you are more comfortable not allowing ranges of AnyType, I won't argue for doing so.

On the issue of braces inside the parentheses, note that we already require that in some cases, when a braced sequence is passed as an argument to a named property, sequence, or endpoint, so this won't be the first occurrence.

Regards,

Erich

| -----Original Message-----
| From: owner-ieee-1850-extensions@eda.org
| [mailto:owner-ieee-1850-extensions@eda.org] On Behalf Of Avigail Orni
| Sent: Monday, January 24, 2005 8:04 AM
| To: ieee-1850-extensions@eda.org
| Subject: RE: Built-in functions for nondeterminism -- revised proposal
|
|
|
|
|
| Erich,
|
| I agree to this suggestion.
| I had been hoping to avoid the need for curly braces inside
| the parentheses, but your argument against range arguments
| has convinced me.
| I also think that the addition of Any_Type to 'forall' is beneficial.
|
| However, I think there is a problem with adding Any_Type to
| ranges, since some types might not have any inherent order.
| It would seem more natural to me to allow Any_Type only in a
| list of values. This would involve a change to Value_Set as follows:
|
|
| Value_Set ::=
| '{' Value_Range { ',' Value_Range } '}'
| | 'boolean'
| | '{' Any_Type { ',' Any_Type } '}'
|
|
| Regards,
| Avigail
| _______________________________________________________
| Avigail Orni
| Verification and Testing Solutions Group IBM Haifa Research Laboratory
| Phone: 972-4-829-6396 email: ornia@il.ibm.com
|
|
|
|
| "Erich Marschner"
|
| <erichm@cadence.c
|
| om>
| To
| Avigail
| Orni/Haifa/IBM@IBMIL
| 24/01/2005 06:56
| cc
|
| <ieee-1850-extensions@eda.org>
|
| Subject
| 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 Mon Jan 24 06:16:09 2005