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

From: Bresticker, Shalom <shalom.bresticker_at_.....>
Date: Thu Aug 14 2008 - 07:21:17 PDT
So the current wording did not get across to me the meaning you were
trying to emphasize. How about something like this:

"This restriction allows a single copy of the assume set to exist that
is valid for the entire simulation, as described ..."

Thanks,
Shalom

> -----Original Message-----
> From: Michael Burns [mailto:michael.burns@freescale.com] 
> Sent: Thursday, August 14, 2008 4:24 PM
> To: Bresticker, Shalom
> Cc: john.havlicek@freescale.com; sv-champions@eda.org; sv-sc@eda.org
> Subject: Re: [sv-sc] some comments on 1900, part 2
> 
> 
> Hi Shalom,
> 
> I felt it was clear that the paragraph was describing how how 
> to form the assume set for a checker instance, and I relied 
> on that context to avoid repeating "for each instantiation". 
> I used "one copy" to distinguish it from many copies, which 
> is what we'd end up with if we make a new set for each new 
> value of a const actual. Saying "a copy" would tend to 
> emphasize the fact that it was a copy more than the number, 
> and I wanted to emphasize the number. I think it's very 
> important that the reference to 17.3.1 stays; it shows that 
> assume sets have the same lifetime semantics as other things 
> in the checker.
> 
> If you feel these issues must be addressed, I'll be happy to 
> do some more wordsmithing; however, I think it'll work as-is, 
> and would rather avoid another round of edits if possible. I 
> would also resist removing the 17.3.1 reference.
> 
> Thanks,
> Mike
> 
> Bresticker, Shalom wrote:
> > Hi, Michael. 
> > 
> > I like most of this:
> > 
> >>>> "The assume set of a checker instance is formed from the
> >> checker assume statements and child checker assume 
> statements. Any of 
> >> these assume statements that reference a formal whose actual 
> >> expression contains any subexpression that is a const or automatic 
> >> value (see 17.3) are excluded from the assume set. This 
> restriction 
> >> allows one copy of the assume set to exist in every time step as 
> >> described in 17.3.1. Among the remaining assume statements, those 
> >> that reference active free variables of the checker are 
> included in 
> >> the assume set..."
> > 
> > But I don't see why this added part:
> > 
> >> This restriction allows one copy of the assume set to 
> exist in every 
> >> time step as described in 17.3.1.
> > 
> > 17.3.1 actually says,
> > 
> > "One copy of these contents exists for each instantiation."
> > 
> > Your added text omits "for each instantiation" and makes it 
> sound as 
> > though there is only one assume set over all instantiations.
> > 
> > Further, the word "one" is emphasizing the number, i.e., 
> one and not 
> > two. Wouldn't "a copy" be enough, and without needing to reference 
> > 17.3.1?
> > 
> > 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.
> > 
> 
---------------------------------------------------------------------
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.
Received on Thu Aug 14 07:23:02 2008

This archive was generated by hypermail 2.1.8 : Thu Aug 14 2008 - 07:23:05 PDT