[sv-ac] RE: rewriting algorithm for checkers and let

Hi Manisha,

just a comment: The actual args to checkers are not passed by value, but they are substituted the same way as to sequence and property instances. There too even though they are substituted (passed by name), the sampled values are used. In checkers it also applies to the operands of assignments.
BTW, the automatic sampling of checker args will change as committee progress in dealing with mantis items.

Best regards,
ed

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
> Kulshrestha, Manisha
> Sent: Friday, July 30, 2010 6:53 AM
> To: sv-ac@eda.org
> Subject: [sv-ac] rewriting algorithm for checkers and let
>
> Hi Dimity/John/all,
>
> I have been looking at the changes required to make rewriting algorithm
> apply to checkers and let. Currently rewriting algorithm is applied to
> flatten the property or sequence instance. It says:
>
> "The result of the algorithm is one flattened sequence or property
> without any instances. "
>
> I can easily extend this for 'let' but applying this algorithm to
> checkers seems to not fit well. There are few questions about it:
>
> 1. There is no such thing as flattening of checker. Or is there ?
> Atleast currently there is no such terminology used for checkers.
> Should this new terminology be introduced for checkers ?
>
> 2. Currently rewriting algorithm is written based on substitution of
> actual in place of formal. But for checkers only arguments of type
> sequence, property and event are substituted. Rest of the arguments are
> passed by value as it says the formals are assigned the sampled value
> of its actual. So, will the reriting algorithm apply to only sequence,
> property or event type of arguments ? What exactly is meant by 'each
> formal argument is assigned the sampled value of its actual argument'.
> Does it behave like tasks/functions where actual is assigned to formals
> at the entry point of task/function and then only formal is used inside
> the body. Does this mean that if actual's value changes while executing
> an assertion in the checker, it does not have any impact on the
> assertion's execution ?
>
> May be current wording is misleading. Could you elaborate on the intent
> in this case.
>
> "When a checker is instantiated, actual arguments are passed to the
> checker. The mechanism for passing
> arguments to a checker is similar to the mechanism for passing
> arguments to a property (see 16.13), and each
> formal argument shall be assigned the sampled value of its actual
> argument during the Preponed region of
> each time step, with the following exceptions and clarifications:
> - If $ is an actual argument to a checker instance, then the
> corresponding formal argument shall
> be untyped and each of its references either shall be an upper bound in
> a
> cycle_delay_const_range_expression or shall itself be an actual
> argument in an instance of a named
> sequence or property, or in a checker instance.
> - If an actual argument contains any subexpression that is a const cast
> or automatic value from
> procedural code, then the corresponding formal argument shall be used
> only in static assertion
> statements (see 16.15.6) or static checker instances within the
> checker. In such cases, the current
> value of each such subexpression shall be substituted before sampling
> the full actual argument,
> whenever a static assertion statement in the checker or a statically
> instantiated subchecker is added
> to the pending procedural assertion queue (see 16.15.6.1 and 17.3.1).
> - Arguments that cannot be sampled, such as events, sequences, and
> properties, are treated similarly
> to such arguments for sequences and properties (see 16.8): they are
> substituted directly for the
> formal argument when it is used in statements or expressions within the
> checker.
> - If the checker is instantiated within another checker, then all
> formal arguments are considered to be
> directly connected to their actual arguments, as in a module
> instantiation. This also means that if the
> actual argument is connected to a formal in the parent checker that
> uses a const cast or automatic
> value from procedural code, it shall only appear in static assertion
> statements or static checker
> instantiations."
>
> Thanks.
> Manisha
>
> --
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
>

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