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

Hi Shalom:

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

I think the point is that if there are no active free checker 
variables in an assume, then the assume specifies nothing to be randomized.

The constant casts are avoided for a different reason.

> 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?

My understanding is that the problem is with the way constant casts
capture values from the procedural context, not with "constants" per se.

What I thought when reading the proposal is that the constant casts
give a way to capture a current value from the procedural context and
pass it into the checker.  This might be a value of a loop iterator.
In such a case, there could be multiple queued instances of the assume
with different values in the const cast arguments.  I imagine that
SV-SC did not want to try to define the randomization in this case.
You could have contention between the multiple copies of the assume.

J.H. 

> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.32,196,1217833200"; 
>    d="scan'208";a="370059520"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Tue, 12 Aug 2008 19:16:29 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-sc] some comments on 1900, part 2
> Thread-Index: Acj5AaouNmP2XNDTSLKDhCbgWliOygDlAxsQ
> From: "Bresticker, Shalom" <shalom.bresticker@intel.com>
> Cc: <sv-champions@eda.org>, <sv-sc@eda.org>
> X-OriginalArrivalTime: 12 Aug 2008 16:16:59.0136 (UTC) FILETIME=[D8B91000:01C8FC96]
> 
> Hi,
> 
> I need clarification about the following:=20
> 
> > > > 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.
> > > >=20
> > > >    Is it true that F1.B1.u2 is in the assume set of=20
> > F1.B1?  I think
> > > >    that the rules say that it is.
> > >=20
> > > Yes, it is. I didn't add anything to the doc about that -=20
> > would you prefer that that be pointed out?
> >=20
> > I think that adding a statement to this effect will help the=20
> > reader to understand what is going on.  F1.B1.u2 involves a=20
> > free checker variable ("n", I seem to recall) that does need=20
> > to be randomized, so just saying that F1.B1.u2 is not in the=20
> > assume set of F1 leaves room for doubt about whether this=20
> > 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.