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

Hi,

I need clarification about the following: 

> > > Part 2, p. 13.  It is stated that the assume set of F1 excludes
> > >    F1.B1.u2 because the only formal argument of the child checker
> > >    bar is bound to actual r that is an inactive free variable.
> > > 
> > >    Is it true that F1.B1.u2 is in the assume set of 
> F1.B1?  I think
> > >    that the rules say that it is.
> > 
> > Yes, it is. I didn't add anything to the doc about that - 
> would you prefer that that be pointed out?
> 
> I think that adding a statement to this effect will help the 
> reader to understand what is going on.  F1.B1.u2 involves a 
> free checker variable ("n", I seem to recall) that does need 
> to be randomized, so just saying that F1.B1.u2 is not in the 
> assume set of F1 leaves room for doubt about whether this 
> variable is ever randomized.

The new added text says,

"However, checker instance F1.B1 has its own assume set, which includes
u2 as well as u1; neither of those assume statements involve formals
with constant actuals."

Similarly, earlier text says,

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

The wording of these two sentences is consistent with each other, but I
have two questions.

1. Why the distinction between an actual which is constant and an actual
that is inactive (e.g., "r" in the example) ?

2. Both of these imply that if an assume statement involves even a
single formal with constant actual, then it is not in the assume set?
Why is an assume statement not in the assume set if it involves even a
single active free checker variable?

Apologies in advance if either of these is explained in following text,
which I have not studied yet.

Thanks,
Shalom
---------------------------------------------------------------------
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.