[sv-ac] preliminary review of formal semantics of argument passing

All:

I have read the document on formal semantics of argument passing
and have only some preliminary comments.

J.H.

Review Formal Semantics of Argument Passing

- I agree with Dmitry that the reference to infinite sequences of 
  non-recursive properties is not so clear.

- There is a mismatch between the bitrange direction of the type 
  "logic [3:0]" and the part select "[1:2]" in the example illustrating 
  $var.  Either the type should be "[0:3]" or the part select should
  be "[2:1]", but not both.

- Step 2 of "flatten_property(P)": I think that we just make every
  local variable declared in P' have a unique identifier.  "Unique with
  respect to ..." is not accurate or clear.

- Step 5 of "flatten_property(P)":  Change "in the instance of P'" to
  "in the instance P".

- Step 5 of "flatten_property(P)":  We seem to lose the formal argument
  type information if f had a type that was not a simple type.  Is this
  situation possible, and, if so, why don't things go wrong?

- Step 3 of "flatten_sequence(R)":  I think "$var(a)" should be "$var(f)"
  as in the property algorithm.  Otherwise, you lose all the references
  to the formal arguments and their declared types (see Steps 4 and 5).

- The procedures for flattening property instances and sequence instances
  seem the same.  Maybe they can be combined?

- I would like to see some more examples to vet the definition.


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