RE: [sv-ac] call to vote on 1549

Hi Bassam.

There is a general comment here that prefers "rewrite/replace" over
"substitute". I like the "substitute" to remain, because it reflects the
spirit of the rewrite algorithm. The term rewrite describes the way that
the formal semantics is defined and not the semantics itself (the formal
semantics of a sequence/property with arguments is defined by a
rewritten sequence/property without arguments.) I think that the spirit
of the semantics is more important than the way it is defined.


Here is my respond to the other specific comments

1) Actual arguments that consist of expressions are checked at compile
time for compatibility
with the types of the corresponding formal arguments. 

>>> What level of compatibility (see 6.22) ? Say *cast compatibility* to
be clear (even if 2nd sentence talks of cast).

[DB] I agree, it used to be equivalent types and now we need to say
something like *cast compatibility*.



4) Also arguments to these sequences shall be static; automatic
variables used as sequence arguments
shall result in an error.

>>> which sequences ? Sentence needs re-wording
>>> rewrite to: Arguments .... . Automatic ...
>>> *** Do we really want to have this restriction ? Why ? This is
extreme. If you mean the operand types we have then fine, this is listed
there strike this out -- in its current form it covers waaaay more than
the operand type restrictions in 16.5.1.

[DB] I agree that the sentence should be rewritten. As for the dynamic
types, I think that the operands of Boolean expressions (16.5.1) should
be restricted to non dynamic types. Any type that does not have an
elaboration bound on its size, may make SVA model-checking un-decidable.


Once we do that, we can lift the restriction on the actual arguments. I
do not see a problem in passing a string to a property as long as it is
not used to determine the property's truth value. It could be useful for
messages etc. 


5) The supported data types for sequence formal arguments are the types
that are allowed for operands
in assertion expressions (see 16.5.1) and the keyword context. ** The
supported data types for
sequence formal arguments are the types that are allowed for operands in
assertion expressions (see **

>>> repetition ....

[DB] Agree, this includes item 4.


6) 16.5.1). In addition, sequence expressions may be typed using the
sequence type and the
event type. A formal type of sequence requires an actual argument that
is either a Boolean
expression or a sequence expression. An actual arg of type property
would cause an error when the
formal type is sequence.
....
A formal argument of property type can accept a Boolean expression,
sequence expression, or
property expression actual argument. The rules for passing arguments to
properties is the same as
those for sequences. Refer to 16.7.1.

>>> I suggest we say something to the effect of cast compatible as a
general statement that we can use for other things in future.

[DB] Well casting is strongly related to assignments, and I am not sure
that I want to see a discussion about sequence/property
assignment/casting. Since the property/sequence types are only used for
formal arguments and not for stand alone variables, I would try to avoid
it.


** formal semantics write-up

7) if e is such an expression, then $var(e) behaves like e in all
respects
except that operations allowed on a reference to or instance of a named
item
declared with the same type as e are also allowed on $var(e). ** In
particular,
any operation that is allowed on a reference to a variable declared with
the
same type as e is allowed on $var(e). **

>>> repetition
>>> do we want to mention type compatibility here or somewhere else in
formal semantics ?

[DB] My intention was to talk about type compatibility only at clause
16, and live it out of the formal semantics. The only sentence that we
wrote is "In particular, if the result is illegal, then so is the
source."


Thanks

Doron

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.