HI Ben,
thanks for immediate reply.
I am still not clear about the use of local formal arguments in properties and sequences. For example, in sequence q_x above, if we make the property non local what difference would it make? On Page no 63, section 2.7 of your SVA assertions handbook, 4th edition, it is said that non local argument is by default of direction input and cannot be written into. Is this true for both sequence and property? Does this mean, in a sequence, if we declare v as non local (remove local attribute), we will not be able to write to it even if its direction is output?
Also in property p_x example you have given above, you are assigning to argument v (statement v = bus1). However, according to the book, formal arguments direction can be only input for a property (for a sequence it could be output, input or inout). Can you please explain.
Also your book says that for untyped formal arguments can be treated as local local formal argument of direction input or output depending upon how it is used in sequence or property. Is this true for property also where formal arguments are always supposed to be of type input?
thanks and regargs,
-sunil puranik