[sv-champions] RE: [sv-sc] some comments on 1900, part 2

Thanks for the explanation. 

I understood why we need to consider assume statements of child checker
instances.

You've explained now why constant actuals are a problem and treated
differently than inactive free variables. I think the text requires such
an explanation to be added, although it could be much shorter and
simpler than what you wrote.

)I still find the term 'const' to refer to items with dynamic lifetime
to be extremely confusing. The very concept of something dynamic being
referred to as 'constant' is very counter-intutitive, giving the
impression of a contradiction in terms.)

Do you mean "constant actuals" or "const actuals"? If an actual is a
real constant, such as a number or a parameter, is that included? What
about a const NON-free variable? If "constant" is used too loosely here,
it may be in other places as well, and this should be checked.

I still don't understand the differences in formulation between child
checker assume statements and parent checker assume statements,
regarding which ones are part of the assume set.

This text:

> "The assume set of a checker instance consists of all assume 
> statements in the checker that do not involve checker formals with 
> constant actuals (see 17.3), as well as those assume statements of 
> child checker instances that involve active free checker variables 
> passed as non-const actuals to the child."

implies that child checker assume statements are part of the assume set
if they involve an active non-const free checker variable EVEN IF they
also involve formals with constant actuals. The latter condition is
mentioned only with respect to the parent checker, not with respect to
the child checkers.

Isn't it possible to to unify the conditions for the assume statements
into a single description which applies both to the parent and the
children?

Thanks,
Shalom


> The restriction on constant actuals is complicated to 
> explain, so I'll do inactive first. The idea of "pulling up" 
> assume statements from child checkers into the parent checker 
> assume set is there so ensure that, when we randomize the 
> free variables in a checker instance, that we include any 
> assumes in child instances that may affect the parent 
> variables being randomized. Inactive free variables are not 
> randomized, so we only need to consider child assumes 
> involving active free variable actuals. Note that the 
> requirement is that it _does_ involve _active_ actuals, 
> rather than _doesn't_ involve _inactive_ actuals. If a child 
> assume statement involves formals with both active and 
> inactive free variable actuals, it is included in the parent 
> assume set.
> 
> The non-const restriction is not related to child instances - 
> it is in effect for assume statements in the parent. The 
> restriction is there because of the lifetime semantics of 
> objects in a procedurally-instantiated checker. There are 
> essentially two kinds of things in a checker - those that are 
> there "quasi-statically" (i.e., one copy per elaborated 
> instance, and for the entire simulation) and those that are 
> there "quasi-dynamically" (i.e., one copy per procedural 
> "invocation" of the instance, starting from the time of 
> invocation). Free checker variables are quasi-static, whereas 
> formals with const actuals (either explicitly const-cast, or 
> implicitly const because e.g. they are automatics) are 
> quasi-dynamic. It would be a nightmare to try to concoct a 
> quasi-static constraint-solving problem from quasi-dynamic 
> assume statements; therefore we do not allow such assumes to 
> participate. They may still exist since they also serve as 
> assertions, which are evaluated quasi-dynamical ly.
> 
> The distinction is there because they are treated slightly 
> differently; inactive actuals are not "poison" - they can be 
> present in an assume without making it ineligible. Const 
> actuals are poison - any const actuals make an assume 
> ineligible regardless of what other formals may be involved.
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.


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