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

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.


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