[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.